Eidesstattliche Erklärung

Ich erkläre an Eides statt, dass ich die vorliegende Dissertation selbstständig und ohne fremde Hilfe verfasst, andere als die angegebenen Quellen und Hilfsmittel nicht benutzt bzw. die wörtlich oder sinngemäß entnommenen Stellen als solche kenntlich gemacht habe.

Judit Robu

Linz, September 2002

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.

Kurzfassung

Wir implementieren in dieser Doktorarbeit diverse geometrische Beweismethoden im Rahmen des Theorema–Systems. Dieses ist in Mathematica programmiert und kann daher auf allen Plattformen, die Mathematica unterstützt, installiert werden. Die hier beschriebenen Funktionen sind in Form von Theorema–Konstrukten verfügbar und operieren im Regelfall mit Formeln in Theorema–Notation.

Die Theorie–Exploration ist ein wichtiges neues Paradigma der computerunterstützten formalen Mathematik. In dieser Dissertation befassen wir uns mit der Theorie–Exploration für den speziellen Fall geometrischer Theorien. In diesem Fall lässt sich der Begriff der Exploration sehr gut eingrenzen, und die Explorationen erreichen einen gewissen Grad an Vollständigkeit. Für eine vorgelegte Folge von geometrischen Konstruktionen gibt es eine Vielzahl von daraus ableitbaren Eigenschaften der zugrundeliegenden geometrischen Elemente (Punkte, Geraden, Strecken, Dreiecke etc). Manche dieser Eigenschaften sind wohlbekannt, aber es kann auch weniger evidente Eigenschaften geben, die sozusagen in der Konstruktion verborgen liegen. Eine effiziente Methode zum Entdecken neuer Theoreme ist die: Man erzeugt zuerst alle Eigenschaften einer gegebenen Konfiguration und analysiert dann, welche dieser Eigenschaften bislang unbekannt ist. Das sukzessive Auffinden aller aus einer gegebenen Konstruktion ableitbaren Eigenschaften nennen wir die systematische Exploration der damit verbundenen Konfiguration. Wir befassen und vorderhand nur mit einigen elementaren Eigenschaften: kollineare Punkte, Parallelen und Senkrechte, proportionale Strecken und Dreiecke von proportionaler Fläche.

Die traditionellen Methoden des geometrischen Beweisens lassen sich nicht auf Sätze mit Ordungsrelationen oder Ungleichungen in der Konklusion anwenden. Die Collins'sche Methode der zylindrisch–algebraischen Zerlegung (CAD = Cylidrical Algebraic Decomposition) ist zwar auf diese Probleme anwendbar aber für die meisten geometrischen Sätze zu langsam. Durch die Kombination der Flächenmethode und des CAD–Algorithmus haben wir eine neue Beweismethode entwickelt, die sich auch anwenden lässt auf viele interessante Theoreme, deren algebraische Formulierung neben polynomialen Gleichungen auch polynomiale Ungleichungen enthält.

Acknowledgements

First of all I would like to thank my supervisor, Prof. Bruno Buchberger for starting the Theorema project and thus making this thesis possible, as well as for sharing his experience in research and guiding my work. I also thank him for the creation and growth of RISC–Linz which offered me a wonderful environment for work and living.

I also would like to thank Prof.Josef Küng for agreeing to co–referee my thesis.

Furthermore I would like to express my gratitude to the members of the Theorema group and to all the people from RISC for their professional and moral support. I want to thank in particular Markus Rosenkranz for helping me with the German translation.

Moreover, I would like to thank Prof. Militon Frentiu from the Babes–Bolyai University, Cluj, Romania, who guided my first steps towards geometry theorem proving.

Last, but not least I am very grateful to my family, my husband, my daughters, my parents, for encouraging me and supporting my long absences from home.