Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/499
DC FieldValueLanguage
dc.contributor.authorStojanović-Đurđević. Sanaen_US
dc.contributor.authorNarboux, Julienen_US
dc.contributor.authorJaničić, Predragen_US
dc.date.accessioned2022-08-13T10:14:40Z-
dc.date.available2022-08-13T10:14:40Z-
dc.date.issued2015-08-01-
dc.identifier.issn10122443en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/499-
dc.description.abstractThe power of state-of-the-art automated and interactive theorem provers has reached the level at which a significant portion of non-trivial mathematical contents can be formalized almost fully automatically. 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 automatically 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.en
dc.relation.ispartofAnnals of Mathematics and Artificial Intelligenceen_US
dc.subjectAutomated theorem provingen
dc.subjectInteractive theorem provingen
dc.subjectTarski’s geometryen
dc.titleAutomated generation of machine verifiable and readable proofs: A case study of tarski’s geometryen_US
dc.typeArticleen_US
dc.identifier.doi10.1007/s10472-014-9443-5-
dc.identifier.scopus2-s2.0-84943199139-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/84943199139-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.firstpage249en_US
dc.relation.lastpage269en_US
dc.relation.volume74en_US
dc.relation.issue3-4en_US
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeArticle-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0002-5386-9100-
crisitem.author.orcid0000-0001-8922-4948-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

8
checked on Dec 21, 2024

Page view(s)

15
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.