Abstract
Constraint Logic Programming can be advantageously used to deal with quadratic constraints stemming from the verification of planar geometry theorems. A hybrid symbolic-numeric representation involving radicals and multiple precision rationals is used to denote the results of quadratic equations. A unification-like algorithm tests for the equality of two expressions using that representation. The proposed approach also utilizes geometric transformations to reduce the number of quadratic equations defining geometric constructions involving circles and straight lines. A large number (512) of geometry theorems has been verified using the proposed approach. Those theorems had been proven correct using a significant more complex (exponential) approach in a treatise authored by Chou in 1988. Even though the proposed approach is based on verification—rather than strict correctness utilized by Chou—the efficiency attained is polynomial thus making the approach useful in classroom situations where a construction attempted by student has to be quickly validated or refuted.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Allen, R., Idt, J., Trilling, L. Constrained based automatic construction and manipulation of geometric figures, Proceedings of the 13th IJCAI Conference, Chambery, Morgan Kaufmann Publishers, Los Altos.
Benhamou, F. Interval constraint logic programming. Constraint Programming: Basics and Trends 1–21.
Bobrow, D. G. (1968). Natural Language Input for a Computer Problem Solving System. Semantic Information Processing. Marvin Minsky (ed.), MIT Press, Cambridge, MA.
Bobrow, D. G. (1968). A Question-Answerer for AlgebraWord Problems. Semantic Information Processing. Marvin Minsky (ed.), MIT Press, Cambridge, MA.
Bouhineau, D. (1997). Construction automatique de figures g´eom´etriques & Programmation Logique avec Constraintes, Thèse de l'Universit´e J. Fourier de Grenoble, France.
Chou, S.-Ch. (1988). Mechanical Geometry Theorem Proving. Reidel Publishing, Norwell.
Colmerauer, A. (1993). Naïve Solving of Non-linear Constraints, Constraint Logic Programming: Selected Research. The MIT Press, F. Benhamou et A. Colmerauer editors, 89–112.
Deng, M., Zhang, J., Yang, L. (1990). The parallel numerical method of mechanical theorem proving. Theoretical Computer Science 74: 253–271.
Dubé, T., Yap, C. Computing in Euclidean Geometry, The Exact Computation Paradigm. World Scientific Press, editors D. Z. Du, F. K. Hwang.
Hong, J. (1986). Proving by example and gap theorems, 107–116. 27th Annual Symposium on Foundations of Computer Science, Toronto, Ontario, Canada. IEEE.
Jaffar, J., Michaylov, S., Stuckey, P-J., Yap, R. (1992). The CLP(R) language and system. ACM Trans. on Programming Languages and Systems 14(3): 339–395.
Kutzler, B. (1988). Algebraic Approaches to Automated Geometry Theorem Proving. Ph.D. thesis, RISCLINZ, Johannes Kepler Univ., Austria.
Landau, S. (1992). Simplification of nested radicals. SIAM Journal of Computing 21(1): 85–110.
Pesant, G., Boyer, M. (1994). Quad-Clp(R): Adding the power of quadratic constraints. Proceedings of the Second Workshop on Principles and Practice of Constraint Programming (PPCP'94).
Pesant, G. (1995). Une approche géométrique aux contraintes arithmétiques quadratiques en programmation logique avec contraintes, Thèse de l'Université de Montréal.
Wu, W-T. (1994). Mechanical Theorem Proving in Geometries. Springer-Verlag Wien New-York.
Zippel, R. (1985). Simplification of expressions involving radicals. J. Symbolic Computation 1.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Bouhineau, D., Trilling, L. & Cohen, J. An Application of CLP: Checking the Correctness of Theorems in Geometry. Constraints 4, 383–405 (1999). https://doi.org/10.1023/A:1009825124248
Issue Date:
DOI: https://doi.org/10.1023/A:1009825124248