AUTOMATSKO REŠAVANJE KONSTRUKTIVNIH PROBLEMA U GEOMETRIJI

eBibliothek Repositorium

 
 

AUTOMATSKO REŠAVANJE KONSTRUKTIVNIH PROBLEMA U GEOMETRIJI

Zur Kurzanzeige

dc.contributor.advisor Janičić, Predrag
dc.contributor.author Marinković, Vesna
dc.date.accessioned 2017-01-11T17:12:27Z
dc.date.available 2017-01-11T17:12:27Z
dc.date.issued 2015
dc.identifier.uri http://hdl.handle.net/123456789/4406
dc.description.abstract The problems of geometry constructions using ruler and compass are one of the oldest and most challenging problems in elementary mathematics. A solution of construction problem is not an illustration, but a procedure that, using given construction primitives, gives a “recipe” how to construct the object sought. The main problem in solving construction problems, both for a human and a computer, is a combinatorial explosion that occurs along the solving process, as well as a procedure of proving solutions correct. In this dissertation a method for automated solving of one class of construction problems, so-called location problems, is proposed. These are the problems in which the task is to construct a triangle if locations of three characteristic points are given. This method successfully proved most of the solvable problems from Wernick’s and Connelly’s list. For each of the problems it is checked if it is symmetric to some of the already solved problems, and then its status is determined: the problem can be found redundant, locus dependent, solvable, or not solvable using existing knowledge. Also, a description of the construction in natural-language form and in language GCLC is automatically generated, accompanied by a corresponding illustration, and correctness proof of the generated construction, followed by the list of conditions when the construction is correct. The proposed method is implemented within the tool ArgoTriCS. For proving generated constructions correct, the system ArgoTriCS uses a newly developed prover ArgoCLP, the automated theorem provers integrated within tools GCLC and OpenGeoProved, as well as the interactive theorem prover Isabelle. It is demonstrated that the proofs obtained can be machine verifiable. Within this dissertation, the system ArgoCLP (developed in collaboration with Sana Stojanovi´c) which is capable of automatically proving theorems in coherent logic is described. This prover is successfully applied to different axiomatic systems. It automatically generates proofs in natural-language form, as well as machineverifiable proofs, whose correctness can be checked using interactive theorem prover Isabelle. The important part of this system is a module for simplification of generated proofs whereby shorter and readable proofs are obtained. en_US
dc.description.provenance Submitted by Slavisha Milisavljevic (slavisha) on 2017-01-11T17:12:27Z No. of bitstreams: 1 tezaVesnaMarinkovic.pdf: 2233812 bytes, checksum: 1cfd8634c1cca86f9aec6c780ba01a6b (MD5) en
dc.description.provenance Made available in DSpace on 2017-01-11T17:12:27Z (GMT). No. of bitstreams: 1 tezaVesnaMarinkovic.pdf: 2233812 bytes, checksum: 1cfd8634c1cca86f9aec6c780ba01a6b (MD5) Previous issue date: 2015 en
dc.language.iso sr en_US
dc.publisher Beograd en_US
dc.title AUTOMATSKO REŠAVANJE KONSTRUKTIVNIH PROBLEMA U GEOMETRIJI en_US
mf.author.birth-date 1982-03-24
mf.author.birth-place Niš 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 Računarstvo en_US
mf.subject.keywords automated reasoning, automated theorem proving, interactive theorem proving, automated generation of readable proofs, coherent logic, geometry construction problems, constructions by ruler and compass en_US
mf.subject.subarea Veštačka inteligencija en_US
mf.contributor.committee Lučić, Zoran
mf.contributor.committee Marić, Filip
mf.contributor.committee Schreck, Pascal
mf.university.faculty Mathematical Faculty en_US
mf.document.references 109 en_US
mf.document.pages 211 en_US
mf.document.location Beograd en_US
mf.document.genealogy-project No en_US
mf.university Belgrade University en_US

Dateien zu dieser Ressource

Dateien Größe Format Anzeige
tezaVesnaMarinkovic.pdf 2.233Mb PDF Öffnen

Das Dokument erscheint in:

Zur Kurzanzeige