=ADD=
=reftype=
14
=number=
02-23
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2002/02-23.ps.gz
=year=
2002
=month=
09
=author=
Robu; Judit
=title=
Geometry Theorem Proving in the Frame of the Theorema Project
=abstract=
In this PhD thesis we are implementing various geometric theorem proving methods in the frame of the Theorema system which is programmed in Mathematica and, hence, can be installed on all machines on which Mathematica is available. The functionalities described in this paper are available as Theorema constructs and, typically, take formulae in Theorema notation as input.
Theory exploration is an important new paradigm in computer-supported formal mathematics. In this thesis, we consider theory exploration for the special case of geometric theories. In this case, theory exploration has a well-defined meaning and a certain degree of "completeness" of explorations can be achieved. Given a list of geometric constructions, there are many properties of the resulting geometric elements (points, lines, segments, triangles, etc), that can be proved.  There are some properties that are well-known but there might also be some hidden properties that are not known so far. A good way for discovering new theorems is generating all the properties of a given configuration and then analyzing which of these properties might be unknown so far. By systematic exploration of a geometric configuration we mean finding, step by step, all the properties that result from the given constructions. For the moment we are concerned only of some basic properties: collinear points, parallel and perpendicular lines, segments with proportional length and triangles with proportional area.
Using traditional geometry theorem proving methods no theorems that involve order relation or contain inequalities in the conclusion can be proved. Collins' Cylindrical Algebraic Decomposition method can deal with such problems but it is too slow for the majority of the geometry theorems.  Combining the area method with Collins' CAD we developed a proof method with which we proved many nontrivial theorems whose algebraic transcription involves, in addition to polynomial equalities, also polynomial inequalities.
=note=
PhD Thesis
=sponsor=
SFB project F1302