Proof simplification and automated theorem proving.
automated theorem proving
proof simplification
Journal
Philosophical transactions. Series A, Mathematical, physical, and engineering sciences
ISSN: 1471-2962
Titre abrégé: Philos Trans A Math Phys Eng Sci
Pays: England
ID NLM: 101133385
Informations de publication
Date de publication:
11 Mar 2019
11 Mar 2019
Historique:
entrez:
11
4
2019
pubmed:
11
4
2019
medline:
11
4
2019
Statut:
ppublish
Résumé
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'.
Identifiants
pubmed: 30966970
doi: 10.1098/rsta.2018.0034
pmc: PMC6365848
doi:
Types de publication
Journal Article
Langues
eng