Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry

Abstract : The power of state-of-the-art automated and interactive the-orem provers has reached the level at which a significant portion of non-trivial mathematical contents can be formalized almost fully automat-ically. In this paper we present our framework for the formalization of mathematical knowledge that can produce machine verifiable proofs (for different proof assistants) but also human-readable (nearly textbook-like) proofs. As a case study, we focus on one of the twentieth century classics – a book on Tarski's geometry. We tried to automatically generate such proofs for the theorems from this book using resolution theorem provers and a coherent logic theorem prover. In the first experiment, we used only theorems from the book, in the second we used additional lemmas from the existing Coq formalization of the book, and in the third we used specific dependency lists from the Coq formalization for each theorem. The results show that 37% of the theorems from the book can be auto-matically proven (with readable and machine verifiable proofs generated) without any guidance, and with additional lemmas this percentage rises to 42%. These results give hope that the described framework and other forms of automation can significantly aid mathematicians in developing formal and informal mathematical knowledge.
Type de document :
Article dans une revue
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2015, 73 (3), pp.25. 〈http://dream.inf.ed.ac.uk/events/amai-geom/〉. 〈10.1007/s10472-014-9443-5〉
Liste complète des métadonnées

Littérature citée [40 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01091011
Contributeur : Julien Narboux <>
Soumis le : jeudi 5 novembre 2015 - 09:07:40
Dernière modification le : samedi 27 octobre 2018 - 01:29:01
Document(s) archivé(s) le : vendredi 28 avril 2017 - 04:59:31

Fichier

AFTarski.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Sana Stojanovic Durdevic, Julien Narboux, Predrag Janicic. Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2015, 73 (3), pp.25. 〈http://dream.inf.ed.ac.uk/events/amai-geom/〉. 〈10.1007/s10472-014-9443-5〉. 〈hal-01091011v2〉

Partager

Métriques

Consultations de la notice

250

Téléchargements de fichiers

199