×

MMP/Geometer – a software package for automated geometric reasoning. (English) Zbl 1202.68378

Winkler, Franz (ed.), Automated deduction in geometry. 4th international workshop, ADG 2002, Hagenberg Castle, Austria, September 4–6, 2002. Revised papers. Berlin: Springer (ISBN 3-540-20927-1/pbk). Lecture Notes in Computer Science 2930. Lecture Notes in Artificial Intelligence, 44-66 (2004).
Summary: We introduce a software package, MMP/Geometer, developed by us to automate some of the basic geometric activities including geometric theorem proving, geometric theorem discovering, and geometric diagram generation. As a theorem prover, MMP/Geometer implements Wu’s method for Euclidean and differential geometries, the area method and the geometric deductive database method. With these methods, we can not only prove difficult geometric theorems but also discover new theorems and generate short and readable proofs. As a geometric diagram editor, MMP/Geometer is an intelligent dynamic geometric software tool which may be used to input and manipulate geometric diagrams conveniently and interactively by combining the idea of dynamic geometry and methods of automated diagram generation.
For the entire collection see [Zbl 1088.68010].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Juno-2; MMP/Geometer
PDFBibTeX XMLCite
Full Text: DOI