Proof simplification and automated theorem proving

DOI10.1098/RSTA.2018.0034MaRDI QIDQ5204800zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Full work available at URL https://arxiv.org/abs/1808.04251, http://europepmc.org/articles/pmc6365848

zbMATH Keywords

automated theorem provingproof 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)

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.

Recommendations

• Prolegomena to any theory of proof simplicity
• scientific article; zbMATH DE number 2024619
• scientific article; zbMATH DE number 1696761
• Hilbert's twenty-fourth problem
• Toward mechanical methods for streamlining proofs

Cites work

• Automating the search for elegant proofs
• Every diassociative A-loop is Moufang
• Finding shortest proofs: An application of linked inference rules
• Hilbert's Twenty-Fourth Problem
• Hilbert's twenty-fourth problem
• scientific article; zbMATH DE number 2024619 (Why is no real title available?)
• scientific article; zbMATH DE number 1865568 (Why is no real title available?)
• Solving open questions and other challenge problems using proof sketches

Cited in

(21)

• Automated proofs of equality problems in Overbeek's competition
• Larry Wos: visions of automated reasoning
• Theorem proving as constraint solving with coherent logic
• Guiding an automated theorem prover with neural rewriting
• scientific article; zbMATH DE number 1696761 (Why is no real title available?)
• Preprocessing of the axiomatic system for more efficient automated proving and shorter proofs
• Automated proof compression by invention of new definitions
• Note on the benefit of proof representations by name
• Automating Change of Representation for Proofs in Discrete Mathematics
• Simplify: a theorem prover for program checking
• scientific article; zbMATH DE number 49488 (Why is no real title available?)
• scientific article; zbMATH DE number 1474909 (Why is no real title available?)
• Proof simplification in the framework of coherent logic
• Remarks on simple proofs
• Increasing the efficiency of automated theorem proving
• Visual thinking and simplicity of proof
• Discussing Hilbert's 24th problem
• Automating algebraic proof systems is NP-hard
• Toward mechanical methods for streamlining proofs
• Short proofs of ideal membership
• Improving automation for higher-order proof steps

Describes a project that uses

Uses Software

• OTTER
• Mace4
• Prover9
• E Theorem Prover
• Waldmeister

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)