FORMALIZACIJA I AUTOMATSKO DOKAZIVANJE TEOREMA EUKLIDSKE GEOMETRIJE

eLibrary

 
 

FORMALIZACIJA I AUTOMATSKO DOKAZIVANJE TEOREMA EUKLIDSKE GEOMETRIJE

Show simple item record

dc.contributor.advisor Janičić, Predrag
dc.contributor.author Stojanović, Sana
dc.date.accessioned 2017-01-30T15:35:39Z
dc.date.available 2017-01-30T15:35:39Z
dc.date.issued 2016
dc.identifier.uri http://hdl.handle.net/123456789/4416
dc.description.abstract The advance of geometry over the centuries can be observed through the development of di erent axiomatic systems that describe it. The use of axiomatic systems begins with Euclid, continues with Hilbert and Tarski, but it doesn't end there. Even today, new axiomatic systems for Euclidean geometry are developed. Avigad's axiomatic system goes back to the beginnings and precisely describes basic derivations presented in Euclid's ½Elements . Writing an axiomatic system in a format suitable for computer theorem proving is a challenge in itself. Imprecise formulations of axioms which appear in books get exposed only when they need to be written in a format suitable for computers. The formalization of di erent axiomatic systems and computer-assisted proofs within theories described by them is the main motif of this thesis. The programs for theorem proving have existed since the eighties and today they present a collection of very powerful tools. This thesis presents a system for automated and formal theorem proving which uses the power of resolution theorem provers, a coherent prover, as well as interactive theorem provers for verifying the generated proofs. Coherent prover ArgoCLP is one of the contributions of the thesis. Additionally, the thesis develops a dialect of coherent logic based on natural deduction which enables simple transformation of generated proofs into proofs written in languages of interactive provers Isabelle and Coq as well as in natural languages, English and Serbian. The system for theorem proving is applied to three axiomatic systems of Euclidean geometry, thus illustrating its applicability to both proving the large mathematical theories and veri cation of informal proofs from mathematical textbooks. en_US
dc.description.provenance Submitted by Slavisha Milisavljevic (slavisha) on 2017-01-30T15:35:39Z No. of bitstreams: 1 SanaStojanovic.pdf: 1885679 bytes, checksum: 1c47057b08466452b673653508d10e40 (MD5) en
dc.description.provenance Made available in DSpace on 2017-01-30T15:35:39Z (GMT). No. of bitstreams: 1 SanaStojanovic.pdf: 1885679 bytes, checksum: 1c47057b08466452b673653508d10e40 (MD5) Previous issue date: 2016 en
dc.language.iso sr en_US
dc.publisher Beograd en_US
dc.title FORMALIZACIJA I AUTOMATSKO DOKAZIVANJE TEOREMA EUKLIDSKE GEOMETRIJE en_US
mf.author.birth-date 1981-05-01
mf.author.birth-place Beograd en_US
mf.author.birth-country Srbija en_US
mf.author.residence-state Srbija en_US
mf.author.citizenship Srpsko en_US
mf.author.nationality Srpkinja en_US
mf.subject.area Computer science en_US
mf.subject.keywords coherent logic, formalization of geometry, automated theorem proving, interactive theorem proving, automated generation of readable proofs en_US
mf.subject.subarea Artificial Intelligence en_US
mf.contributor.committee Lučić, Zoran
mf.contributor.committee Marić, Filip
mf.contributor.committee Narbu, Žilien
mf.university.faculty Mathematical Faculty en_US
mf.document.references 100 en_US
mf.document.pages 150 en_US
mf.document.location Beograd en_US
mf.document.genealogy-project No en_US
mf.university Belgrade University en_US

Files in this item

Files Size Format View
SanaStojanovic.pdf 1.885Mb PDF View/Open

This item appears in the following Collection(s)

Show simple item record