|
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. |