Towards fast automatic verification of textbook proof steps

DOI10.1007/978-3-032-32589-1_5MaRDI QIDQ7411155zbMATH OpenFDO

Authors Adam Dingle

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_5

zbMATH Keywords

higher-order logicsuperpositiontheorem proving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A theory of type polymorphism in programming
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Edinburgh LCF. A mechanized logic of computation
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Efficient full higher-order unification
• Hammering towards QED
• HOL Light: An Overview
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 3422667 (Why is no real title available?)
• scientific article; zbMATH DE number 3548474 (Why is no real title available?)
• scientific article; zbMATH DE number 5486212 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Logics and type systems in theory and practice. Essays dedicated to Herman Geuvers on the occasion of his 60th birthday
• Making higher-order superposition work
• Mechanizing \(\omega\)-order type theory through unification
• Performance of clause selection heuristics for saturation-based theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Sine qua non for large theory reasoning
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Superposition for higher-order logic
• Teaching mathematics using Lean and controlled natural language
• The Lean 4 theorem prover and programming language
• The seven virtues of simple type theory
• The state of CASC
• The system \({\mathcal F}\) of variable types, fifteen years later
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0

This page was built for publication: Towards fast automatic verification of textbook proof steps

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7411155)