CISUC

The Area Method: a Recapitulation

Authors

Predrag Janicic
Julien Narboux
Pedro Quaresma

Abstract

The area method for Euclidean constructive geometry was proposed by Chou, Gao and Zhang in the early 1990's. The method can efficiently prove many non-trivia geometry theorems and is one of the most interesting and most successful methods for automated theorem proving in geometry The method produces proofs that are often very concise and human-readable.

In this paper, we provide a first complete presentation of the method. We provide both algorithmic and implementation details that were omitted in the original presentations. We also give a variant of Chou, Gao and Zhang's axiom system. Based on this axiom system, we proved formally all the lemmas needed by the method and its soundness using the Coq proof assistant.

To our knowledge, apart from the original implementation by the authors who first proposed the method, there are only three implementations more. Although the basic idea of the method is simple, implementing it is a very challenging task because of a number of details that has to be dealt with. With the description of the method given in this paper, implementing the method should be still complex, but a straightforward task. In the paper we describe all these implementations and also some of their applications.

Keywords

area method, geometry, automated theorem proving, formalisation

Subject

geometric automated theorem proving

Journal

Journal of Automated Reasoning, Vol. 48, #4, pp. 489-532, April 2012

Cited by

Year 2015 : 3 citations

 Botana, F., Hohenwarter, M., Janicic, P., Kovács, Z., Petrovic, I., Recio, T., & Weitzhofer, S. (2015). Automated theorem proving in GeoGebra: current achievements. Journal of Automated Reasoning, 55(1), 39-59.

 Boutry, P., Narboux, J., & Schreck, P. (2015). A reflexive tactic for automated generation of proofs of incidence to an affine variety.

 Maric, F., & Petrovic, D. (2015). Formalizing complex plane geometry. Annals of Mathematics and Artificial Intelligence, 74(3-4), 271-308.

Year 2014 : 1 citations

 Maric, Filip and Petrovic, Danijela, Formalizing complex plane geometry, Annals of Mathematics and Artificial Intelligence, pg 1-38, Springer (DOI:10.1007/s10472-014-9436-4)

Year 2013 : 2 citations

 Groves, Lindsay and Sun, Jing, Verifying an Aircraft Proximity Characterization Method in Coq, LNCS 8144, Springer, DOI: 10.1007/978-3-642-41202-8_7

 Braun, Gabriel and Narboux, Julien, From Tarski to Hilbert, LNCS 7993, Springer 2013, Doi: 10.1007/978-3-642-40672-0_7

Year 2012 : 7 citations

 Formalization and Implementation of Algebraic Methods in Geometry, Maric, Filip and Petrovic, Ivan and Petrovic, Danijela and Janicic, Predrag, Proceedings First Workshop on CTP Components for Educational Software, Wrocl}aw, Poland, 31th July 2011, Electronic Proceedings in Theoretical Computer Science, 79, 2012.

 A case study in formalizing projective geometry in Coq: Desargues theorem, Nicolas Magaud and Julien Narboux and Pascal Schreck, Computational Geometry, Elsevier, 2012.

 Schreck, Pascal, Pascal Mathis, and Julien Narboux. "Geometric Construction Problem Solving in Computer-Aided Learning." 24th IEEE International Conference on Tools with Artificial Intelligence. 2012.

 Jiang, Jianguo, and Jingzhong Zhang. "A review and prospect of readable machine proofs for geometry theorems." Journal of Systems Science and Complexity 25.4 (2012): 802-820.

 Malikovic, Marko, Mirko Cubrilo, and Predrag Janicic. "Formalization of a Strategy for the KRK Chess Endgame."Central European Conference on Information and Intelligent Systems. 2012.

 Braun, Gabriel, and Julien Narboux. "From Tarski to Hilbert." Automated Deduction in Geometry 2012. 2012.

 Marinkovic, Vesna, and Predrag Janicic. "Towards understanding triangle construction problems." Intelligent Computer Mathematics (2012): 127-142.

Year 2011 : 3 citations

 A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry
Pham, Tuan Minh and Bertot, Yves and Narboux, Julien, The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), LNCS 6785, pg 368,383, Springer 2011

 A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry, Fuchs, Laurent and Thery, Laurent, Automated Deduction in Geometry 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers, LNCS 6877, pg 51-62, Springer, 2011

 Formalization of Wu's simple method in Coq, GÉnevaux, Jean-David and Narboux, Julien and Schreck, Pascal, CPP 2011, LNCS 7086, Springer, 2011