Proof simplification and automated theorem proving

DOI10.1098/RSTA.2018.0034zbMATH Open1436.03101arXiv1808.04251OpenAlexW3102050129WikidataQ92982873 ScholiaQ92982873MaRDI QIDQ5204800

Michael K. Kinyon

Publication date: 5 December 2019

Published in: Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences (Search for Journal in Brave)

Abstract: The proofs first generated by automated theorem provers are far from optimal by any measure of simplicity. In this paper I describe a technique for simplifying automated proofs. Hopefully this discussion will stimulate interest in the larger, still open, question of what reasonable measures of proof simplicity might be.

Full work available at URL: https://arxiv.org/abs/1808.04251

zbMATH Keywords

automated theorem proving proof simplification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

Related Items (11)

Automating Change of Representation for Proofs in Discrete Mathematics ⋮ Automating algebraic proof systems is NP-hard ⋮ Title not available (Why is that?) ⋮ Simplify: a theorem prover for program checking ⋮ Short proofs of ideal membership ⋮ Discussing Hilbert's 24th problem ⋮ Title not available (Why is that?) ⋮ Larry Wos: visions of automated reasoning ⋮ Theorem proving as constraint solving with coherent logic ⋮ Guiding an automated theorem prover with neural rewriting ⋮ Automated proofs of equality problems in Overbeek's competition

Uses Software

This page was built for publication: Proof simplification and automated theorem proving

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