Gao, Xiao-Shan; Lin, Qiang 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]. Cited in 14 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:geometry software; automated reasoning; geometric theorem proving; geometric theorem discovering; geometric diagram generation; intelligent dynamic geometry; MMP/Geometer Software:Juno-2; MMP/Geometer PDFBibTeX XMLCite \textit{X.-S. Gao} and \textit{Q. Lin}, Lect. Notes Comput. Sci. 2930, 44--66 (2004; Zbl 1202.68378) Full Text: DOI