FORMALIZACIJA I AUTOMATSKO DOKAZIVANJE TEOREMA EUKLIDSKE GEOMETRIJE

eLibrary

 
 

FORMALIZACIJA I AUTOMATSKO DOKAZIVANJE TEOREMA EUKLIDSKE GEOMETRIJE

Show full item record

Title: FORMALIZACIJA I AUTOMATSKO DOKAZIVANJE TEOREMA EUKLIDSKE GEOMETRIJE
Author: Stojanović, Sana
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.
URI: http://hdl.handle.net/123456789/4416
Date: 2016

Files in this item

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

The following license files are associated with this item:

This item appears in the following Collection(s)

Show full item record