Solving geometrical constraint systems using CLP based on linear constraint solver
Euclidean geometrical configurations obtained with ruler, square and compass may be described as arithmetic constraint systems over rational numbers and consequently belong to the domain of CLP(R). Unfortunately, CLP based on linear constraint solvers which are efficient and can deal with geometrical constraints such as parallelism, perpendicularity, belonging to a line i.e. pseudo-linear constraints, cannot handle quadratic constraints introduced when using circles.
Two problems arise with quadratic constraints: the first problem is how to solve mixed constraint systems i.e. linear constraints combined with quadratic constraints; the second problem is how to represent the real numbers involved in the resolution of mixed constraints, so that correctness and completeness of linear constraint solvers are preserved.
In this paper we present a naive algorithm for mixed constraints based on a cooperation with a linear constraint solver. We define a representation for the real numbers, i.e. constructible numbers, occuring in Euclidean geometry. This representation preserves correctness and completeness of above algorithms. A survey over 512 theorems of Euclidean geometry shows that from both theoretical and experimental points of view, this representation is appropriate. This work is intended to be used to verify geometrical properties in Intelligent Tutoring System for geometry.
Keywordsquadratic algebraic extension representation of rational, real, algebraic, and constructible numbers cooperation between solvers for mixed constraints
Unable to display preview. Download preview PDF.
- [All93]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, 1993.Google Scholar
- [Bor85]Borodin, A., Fagin, R., Hopcroft, J.E., Tompa, M., Decreasing the nested depth of expression involving square roots, Journal of Symbolic Computation, no. 1 page 169–188, 1985.Google Scholar
- [Chou92]S.C. Chou and X.S. Gao, Proving Geometry Statement of Constructive Type, CADE, LNCS 607, D. Kapur Eds, 1992.Google Scholar
- [Chou88]S.C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, 1988.Google Scholar
- [Col90]A. Colmerauer, An Introduction to Prolog III, Commun. ACM, 28(4):412–418, 1990.Google Scholar
- [Col93]A. Colmerauer, Naive Solving of Non-linear Constraints, Constraint Logic Programming: Selected Research, F. Benhamou and A. Colmerauer eds, The MIT Press, page 89–112, 1993.Google Scholar
- [Dav77]Davis, P.J., Proof, Completeness, Transcendental, and Sampling. Journal of the ACM, Vol. 24, no. 2, pages 298–310, 1977.Google Scholar
- [Din88]M. Dincbas, P. Van Hentenryck, H. Simonis, A. Aggoun, T. Graf, and F. Berthier. The Constraint Logic Programming Language CHIP, In Proceedings of the Internationnal Conference on 5 Fifth Generation Computer Systems, Tokyo, Japan, December 1988.Google Scholar
- [Jaf92]J. Jaffar, S. Michaylov, P-J. Stuckey, and R. Yap, The CLP(R) Language and System. ACM Trans. on Programming Languages and Systems, 14(3):339–395, 1992.Google Scholar
- [Hon86]J. Hong, Proving by Example and Gap Theorems 27th An. Symp. on Foundations of Computer Science, Toronto, Ontario, Canada, IEEE press, p107–116, Oct 1986.Google Scholar
- [Lab95]J.M. Laborde, Des connaissances abstraites aux réalités artificielles, le concept de micromonde Cabri, IVèmes journées EIAO de Cachan, ed Eyrolles, 1995.Google Scholar
- [Lan92]Landau, S., Simplification of nested radicals, SIAM Journal of Computing Vol 21, no.1 page 85–110, February 1992.Google Scholar
- [Leb92]Lebesgue, H., Leçons sur les constructions géométriques, réédition, Gauthier-Villard, Paris, 1989.Google Scholar
- [Nau85]Naudin, P., Quitté, C. Algorithmique algébrique Collection Logique mathématiques informatique, édition Masson, pages 312–324, 1985.Google Scholar
- [Pes95]Pesant, G., Une approche géométrique aux contraintes arithmétiques quadratiques en programmation logique avec contraintes Thèse de l'Universite de Montréal, 1995.Google Scholar
- [Rol87]Rolfe, T., On a fast integer square root algorithm. ACM SIGNUM Newsletter, Vol. 22, no. 4, pages 6–11, 1987.Google Scholar