Title
Аутоматско решавање конструктивних проблема у геометрији
Creator
Marinković, Vesna, 1982-
Copyright date
2015
Object Links
Select license
Autorstvo 3.0 Srbija (CC BY 3.0)
License description
Dozvoljavate umnožavanje, distribuciju i javno saopštavanje dela, i prerade, ako se navede ime autora na način odredjen od strane autora ili davaoca licence, čak i u komercijalne svrhe. Ovo je najslobodnija od svih licenci. Osnovni opis Licence: http://creativecommons.org/licenses/by/3.0/rs/deed.sr_LATN Sadržaj ugovora u celini: http://creativecommons.org/licenses/by/3.0/rs/legalcode.sr-Latn
Language
Serbian
Cobiss-ID
Theses Type
Doktorska disertacija
description
Datum odbrane: 04.06.2015.
Other responsibilities
mentor
Janičić, Predrag. 1968-
član komisije
Lučić, Zoran, 1952-
član komisije
Marić, Filip, 1978-
član komisije
Schreck, Pascal.
Academic Expertise
Prirodno-matematičke nauke
Academic Title
-
University
Univerzitet u Beogradu
Faculty
Matematički fakultet
Alternative title
Automated solving of construction problems in geometry
Publisher
[В. Маринковић]
Format
213 листa
description
Рачунарство - Вештачка интелигенција / Artificial Intelligence
Abstract (sr)
Проблеми геометријских конструкција уз помоћ лењира и шестара представљају један од најстаријих и најизазовнијих проблема у елементарној математици. Под решењем конструктивног проблема не подразумева се слика, већ процедура којом се, на основу задатих конструкцијских примитива, у низу корака даје "упутство" како треба конструисати тражени објекат...
Abstract (en)
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.
Authors Key words
аутоматско резоновање, аутоматско доказивање теорема, интерактивно доказивање теорема, аутоматско генерисање читљивих доказа, кохерентна логика, конструктивни проблеми у геометрији, конструкције лењиром и шестаром
Authors Key words
automated reasoning, automated theorem proving, interactive theorem
proving, automated generation of readable proofs, coherent logic, geometry
construction problems, constructions by ruler and compass
Classification
004.832.3:514.181.8(043.3)
Type
Tekst
Abstract (sr)
Проблеми геометријских конструкција уз помоћ лењира и шестара представљају један од најстаријих и најизазовнијих проблема у елементарној математици. Под решењем конструктивног проблема не подразумева се слика, већ процедура којом се, на основу задатих конструкцијских примитива, у низу корака даје "упутство" како треба конструисати тражени објекат...
“Data exchange” service offers individual users metadata transfer in several different formats. Citation formats are offered for transfers in texts as for the transfer into internet pages. Citation formats include permanent links that guarantee access to cited sources. For use are commonly structured metadata schemes : Dublin Core xml and ETUB-MS xml, local adaptation of international ETD-MS scheme intended for use in academic documents.