Restricted access
Research articles
Research articlesProof simplification and automated theorem proving
Published:21 January 2019https://doi.org/10.1098/rsta.2018.0034
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.
This article is part of the theme issue ‘The notion of ‘simple proof’ - Hilbert's 24th problem’.
Footnotes
References
- 1. Canadian Society for the History and Philosophy of Mathematics. 2000Program of the 2000 Annual Meeting at McMaster University, Ontario, Canada. See http://www.cshpm.org/archives/programs/prog2000.pdf. Google Scholar
- 2.
Thiele R . 2000Hilbert and his twenty-four problems. In Mathematics at the Dawn of a Millennium. Proceedings of the Canadian Society for History and Philosophy of Mathematics, Hamilton, Ont., vol. 13 (ed. M Kinyon), pp. 1–22. Google Scholar - 3.
Thiele R . 2003Hilbert's twenty-fourth problem. Am. Math. Mon. 110, 1–24. (doi:10.1080/00029890.2003.11919933) Crossref, ISI, Google Scholar - 4.
Kinyon MK, Kunen K, Phillips JD . 2002Every diassociative A-loop is Moufang. Proc. Am. Math. Soc. 130, 619–624. (doi:10.1090/S0002-9939-01-06090-7) Crossref, ISI, Google Scholar - 5.
McCune WW . 2004OTTER (Organized Techniques for Theorem-proving and Effective Research), Last supported version: 3.3f (August 2004). See http://www.cs.unm.edu/mccune/otter/. Google Scholar - 6.
McCune WW . 2009Prover9 and Mace4, Current version: 2009-11A. See http://www.cs.unm.edu/mccune/prover9/. Google Scholar - 7.
Schulz S . 2017The E Theorem Prover, Current version: 2.0 Turzum (2017-07-04). See http://wwwlehre.dhbw-stuttgart.de/sschulz/E/E.html. Google Scholar - 8.
Hillenbrand T . 2018Waldmeister, Current version: February 2018. See https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/waldmeister/. Google Scholar - 9.
- 10.
Thiele R, Wos L . 2002Hilbert's twenty-fourth problem. J. Automat. Reason. 29, 67–89. (doi:10.1023/A:1020537107897) Crossref, ISI, Google Scholar - 11.
Veroff R . 2001Finding shortest proofs: an application of linked inference rules. J. Automat. Reason. 27, 123–139. (doi:10.1023/A:1010635625063) Crossref, ISI, Google Scholar - 12.
Wos L, Thiele R . 2001Hilbert's new problem. Bull. Sect. Logic Univ. Łódź 30, 165–175. Google Scholar - 13.
Wos L . 1998Automating the search for elegant proofs. J. Automated Reason. 21, 135–175. (doi:10.1023/A:1005847113370) Crossref, ISI, Google Scholar - 14.
Veroff R . 2001Solving open questions and other challenge problems using proof sketches. J. Automat. Reason. 27, 157–174. (doi:10.1023/A:1010639725972) Crossref, ISI, Google Scholar - 15.
Wos L, Pieper GW 2003Automated reasoning and the discovery of missing and elegant proofs. Paramus, NJ: Rinton Press. Incorporated. Google Scholar
