|
Abstract:
|
In this thesis is presented interactive formalization of various models of geometry
and algebraic methods for automated proving geometry theorems.
We present our current work on formalizing analytic (Cartesian) plane geometries
within the proof assistant Isabelle/HOL. We give several equivalent definitions
of the Cartesian plane and show that it models synthetic plane geometries
(using both Tarski’s and Hilbert’s axiom systems). We also discuss several techniques
used to simplify and automate the proofs. As one of our aims is to advocate
the use of proof assistants in mathematical education, our exposure tries to remain
simple and close to standard textbook definitions, but completely formal and
mechanically verifiable. This formalization presents the develop of the necessary
infrastructure for implementing decision procedures based on analytic geometry
within proof assistants.
Furthermore, we investigate complex numbers. Deep connections between complex
numbers and geometry had been well known and carefully studied centuries
ago. Fundamental objects that are investigated are the complex plane (usually extended
by a single infinite point), its objects (points, lines and circles), and groups
of transformations that act on them (e.g., inversions and Möbius transformations).
In this thesis we treat the geometry of complex numbers formally and present a
fully mechanically verified development within the theorem prover Isabelle/HOL.
We discuss different approaches to formalization and discuss major advantages of
the more algebraically oriented approach. Apart from applications in formalizing
mathematics and in education, this work serves as a ground for formally investigating
various non-Euclidean geometries and their intimate connections. We
also present a formalization of part of Tarski axiom system withing Poincare disk
model in Isabelle/HOL.
Further on, we analyze connections between geometry and polynomials and the
use of these connections. In Euclidean geometry, objects and relations between
them can be expressed as polynomials. Further, any geometry construction can be
expressed by set of polynomials and geometry statements can be proved by using
algebraic methods (e.g. the Gröbner bases method or Wu’s method) over that set
of polynomials. We describe an implementation of an algorithm in Isabelle/HOL
that accepts a term representation of a geometry construction and returns its corresponding
set of polynomials. Our further work will be to use the method of
Gröbner bases within the Isabelle system on the generated polynomials, in order
to prove correctness of the given construction. Furthermore, we investigate how
spatial geometry constructions can be presented using polynomials. We investigate
two different approaches in deriving those polynomials and then compare
efficiency of algebraic provers depending on the approach used. We present a fully
automated system for transforming geometry constructions into set of polynomials.
Our further work would be to relate these geometry provers with dynamic
geometry software and thus make easier for students to use it. |