FORMALIZACIJA RAZLIČITIH MODELA GEOMETRIJE I PRIMENE U VERIFIKACIJI AUTOMATSKIH DOKAZIVAČA TEOREMA

eBiblioteka

 
 

FORMALIZACIJA RAZLIČITIH MODELA GEOMETRIJE I PRIMENE U VERIFIKACIJI AUTOMATSKIH DOKAZIVAČA TEOREMA

Show simple item record

dc.contributor.advisor Marić, Filip
dc.contributor.author Simić, Danijela
dc.date.accessioned 2017-10-16T15:30:49Z
dc.date.available 2017-10-16T15:30:49Z
dc.date.issued 2017
dc.identifier.uri http://hdl.handle.net/123456789/4499
dc.description.abstract In this thesis is presented interactive formalization of various models of geometry and algebraic methods for automated proving geometry theorems. We present our current work on formalizing analytic (Cartesian) plane geometries within the proof assistant Isabelle/HOL. We give several equivalent definitions of the Cartesian plane and show that it models synthetic plane geometries (using both Tarski’s and Hilbert’s axiom systems). We also discuss several techniques used to simplify and automate the proofs. As one of our aims is to advocate the use of proof assistants in mathematical education, our exposure tries to remain simple and close to standard textbook definitions, but completely formal and mechanically verifiable. This formalization presents the develop of the necessary infrastructure for implementing decision procedures based on analytic geometry within proof assistants. Furthermore, we investigate complex numbers. Deep connections between complex numbers and geometry had been well known and carefully studied centuries ago. Fundamental objects that are investigated are the complex plane (usually extended by a single infinite point), its objects (points, lines and circles), and groups of transformations that act on them (e.g., inversions and Möbius transformations). In this thesis we treat the geometry of complex numbers formally and present a fully mechanically verified development within the theorem prover Isabelle/HOL. We discuss different approaches to formalization and discuss major advantages of the more algebraically oriented approach. Apart from applications in formalizing mathematics and in education, this work serves as a ground for formally investigating various non-Euclidean geometries and their intimate connections. We also present a formalization of part of Tarski axiom system withing Poincare disk model in Isabelle/HOL. Further on, we analyze connections between geometry and polynomials and the use of these connections. In Euclidean geometry, objects and relations between them can be expressed as polynomials. Further, any geometry construction can be expressed by set of polynomials and geometry statements can be proved by using algebraic methods (e.g. the Gröbner bases method or Wu’s method) over that set of polynomials. We describe an implementation of an algorithm in Isabelle/HOL that accepts a term representation of a geometry construction and returns its corresponding set of polynomials. Our further work will be to use the method of Gröbner bases within the Isabelle system on the generated polynomials, in order to prove correctness of the given construction. Furthermore, we investigate how spatial geometry constructions can be presented using polynomials. We investigate two different approaches in deriving those polynomials and then compare efficiency of algebraic provers depending on the approach used. We present a fully automated system for transforming geometry constructions into set of polynomials. Our further work would be to relate these geometry provers with dynamic geometry software and thus make easier for students to use it. en_US
dc.description.provenance Submitted by Slavisha Milisavljevic (slavisha) on 2017-10-16T15:30:49Z No. of bitstreams: 1 06062017danijela_doktorat.pdf: 1158024 bytes, checksum: fe2c2b32597ad98c139560a59f5e86ec (MD5) en
dc.description.provenance Made available in DSpace on 2017-10-16T15:30:49Z (GMT). No. of bitstreams: 1 06062017danijela_doktorat.pdf: 1158024 bytes, checksum: fe2c2b32597ad98c139560a59f5e86ec (MD5) Previous issue date: 2017 en
dc.language.iso sr en_US
dc.publisher Beograd en_US
dc.title FORMALIZACIJA RAZLIČITIH MODELA GEOMETRIJE I PRIMENE U VERIFIKACIJI AUTOMATSKIH DOKAZIVAČA TEOREMA en_US
mf.author.birth-date 1986-09-26
mf.author.birth-place Valjevo 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 proof assistants, geometry, interactive proving in geometry, automated proving in geometry, hyperbolic geometry, spatial geometry, Tarski axiom system, Hilbert axiom system, Cartesian coordinate system en_US
mf.subject.subarea automated reasoning en_US
mf.contributor.committee Janičić, Predrag
mf.contributor.committee Vukmirović, Srđan
mf.contributor.committee Maksimović, Petar
mf.university.faculty Mathematical Faculty en_US
mf.document.references 174 en_US
mf.document.pages 216 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
06062017danijela_doktorat.pdf 1.158Mb PDF View/Open

This item appears in the following Collection(s)

Show simple item record