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