×

zbMATH — the first resource for mathematics

Computer theorem proving for verifiable solving of geometric construction problems. (English) Zbl 1434.03032
Botana, Francisco (ed.) et al., Automated deduction in geometry. 10th international workshop, ADG 2014, Coimbra, Portugal, July 9–11, 2014. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 9201, 72-93 (2015).
Summary: Over the last sixty years, a number of methods for automated theorem proving in geometry, especially Euclidean geometry, have been developed. Almost all of them focus on universally quantified theorems. On the other hand, there are only few studies about logical approaches to geometric constructions. Consequently, automated proving of \(\forall \exists \) theorems, that correspond to geometric construction problems, have seldom been studied. In this paper, we present a formal logical framework describing the traditional four phases process of geometric construction solving. It leads to automated production of constructions with corresponding human readable correctness proofs. To our knowledge, this is the first study in that direction. In this paper we also discuss algebraic approaches for solving ruler-and-compass construction problems. There are famous problems showing that it is often difficult to prove non-existence of constructible solutions for some tasks. We show how to put into practice well-known algebra-based methods and, in particular, field theory, to prove RC-constructibility in the case of problems from Wernick’s list.
For the entire collection see [Zbl 1316.68005].

MSC:
03B35 Mechanization of proofs and logical operations
51M15 Geometric constructions in real or complex geometry
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aldefeld, B.: Variations of geometries based on a geometric-reasoning method. Comput. Aided Des. 20(3), 117-126 (1988) · Zbl 0656.65017 · doi:10.1016/0010-4485(88)90019-X
[2] Boutry, P., Narboux, J., Schreck, P., Braun, G.: Using small scale automation to improve both accessibility and readability of formal proofs in geometry. In: Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), CISUC TR2014/02, Universidade de Coimbra (2014)
[3] Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) ADG 2012. LNCS, vol. 7993, pp. 89-109. Springer, Heidelberg (2013) · Zbl 1397.03019 · doi:10.1007/978-3-642-40672-0_7
[4] Buoma, W., Fudos, I., Hoffman, C., Cai, J., Paige, R.: A geometric constraint solver. CAD 27, 487-501 (1995) · Zbl 0960.68721
[5] Buthion, M.: Un programme qui résoud formellement des problèmes de constructions géométriques. RAIRO Informatique 3(4), 353-387 (1979) · Zbl 0403.51014
[6] Chen, G.: Les constructions à la règle et au compas par une méthode algébrique. Technical report Rapport de DEA, Université Louis Pasteur (1992)
[7] Djorić, M., Janičić, P.: Constructions, instructions, interactions. Teach. Mathe. Appl. 23(2), 69-88 (2004)
[8] Dufourd, J.-F., Mathis, P., Schreck, P.: Geometric construction by assembling solved subfigures. Artif. Intell. J. 99(1), 73-119 (1998) · Zbl 0903.68149 · doi:10.1016/S0004-3702(97)00070-2
[9] Essert-Villard, C., Schreck, P., Dufourd, J.-F.: Sketch-based pruning of a solution space within a formal geometric constraint solver. Artif. Intell. 124(1), 139-159 (2000) · Zbl 0952.68152 · doi:10.1016/S0004-3702(00)00061-8
[10] Gao, X.-S., Chou, S.-C.: Solving geometric constraint systems. ii. A symbolic approach and decision of rc-constructibility. Comput. Aided Des. 30(2), 115-122 (1998) · Zbl 05470929 · doi:10.1016/S0010-4485(97)00055-9
[11] Gelernter, H.: Realization of a geometry theorem proving machine. In: Proceedings of the International Conference Information Processing, Paris, pp. 273-282, 15-20 June 1959
[12] Génevaux, J.-D., Narboux, J., Schreck, P.: Formalization of Wu’s simple method in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 71-86. Springer, Heidelberg (2011) · Zbl 1350.68234 · doi:10.1007/978-3-642-25379-9_8
[13] Grégoire, B., Pottier, L., Théry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol. 6301, pp. 42-59. Springer, Heidelberg (2011) · Zbl 1302.68242 · doi:10.1007/978-3-642-21046-4_3
[14] Gulwani, S., Korthikanti, V.A., Tiwari, A.: Synthesizing geometry constructions. In: Programming Language Design and Implementation, PLDI 2011, pp. 50-61. ACM (2011)
[15] Janičić, P.: Geometry constructions language. J. Autom. Reasoning 44(1-2), 3-24 (2010) · Zbl 1185.68626
[16] Jermann, C., Trombettoni, G., Neveu, B., Mathis, P.: Decomposition of geometric constraint systems: a survey. Int. J. Comput. Geom. Appl. 16(5-6), 379-414 (2006). CNRS MathSTIC · Zbl 1104.65304 · doi:10.1142/S0218195906002105
[17] Landau, S., Miller, G.L.: Solvability by radicals is in polynomial time. J. Comput. Syst. Sci. 30(2), 179-208 (1985) · Zbl 0586.12002 · doi:10.1016/0022-0000(85)90013-3
[18] Lebesgue, H.: Leçons sur les constructions géométriques. Gauthier-Villars, Paris (1950) (in French), re-edition by Editions Jacques Gabay, France
[19] Lemaire, F., Moreno-Maza, M., Xie, Y.: The RegularChains library in Maple 10. In: Kotsireas, I.S. (ed.) Proceedings of Maple Summer Conference 2005, Waterloo, Canada, pp. 355-368 (2005) · Zbl 1114.68628
[20] Marić, F., Petrović, I., Petrović, D., Janičić, P.: Formalization and implementation of algebraic methods in geometry. In: Quaresma, P., Back, R.-J. (eds.) Proceedings of First Workshop on CTP Components for Educational Software, Wrocław, Poland, 31 July 2011. Electronic Proceedings in Theoretical Computer Science, vol. 79, pp. 63-81. Open Publishing Association (2012)
[21] Marinković, V., Janičić, P.: Towards understanding triangle construction problems. In: Campbell, J.A., Jeuring, J., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 127-142. Springer, Heidelberg (2012) · Zbl 1359.68265 · doi:10.1007/978-3-642-31374-5_9
[22] Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL. LNCS, vol. 2283, p. 3. Springer, Heidelberg (2002) · doi:10.1007/3-540-45949-9_1
[23] Owen, J.: Algebraic solution for geometry from dimensional constraints. In: Proceedings of the 1th ACM Symposium of Solid Modeling and CAD/CAM Applications, pp. 397-407. ACM Press (1991)
[24] Scandura, J.M., Durnin, J.H., Wulfeck II, W.H.: Higher order rule characterization of heuristics for compass and straight edge constructions in geometry. Artif. Intell. 5(2), 149-183 (1974) · Zbl 0288.68051 · doi:10.1016/0004-3702(74)90028-9
[25] Schreck, P.: Robustness in CAD Geometric Constructions. In: IV 2001, pp. 111-116 (2001)
[26] Schreck, P.: Modélisation et implantation d’un système à base de connaissances pour les constructions géométriques. Revue d’Intelligence Artificielle 8(3), 223-247 (1994)
[27] Schreck, P., Mathis, P.: Rc-constructibility of problems in Wernick’s and Connelly’s lists. In: Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), CISUC TR2014/02, Universidade de Coimbra (2014)
[28] Stojanović, S., Pavlović, V., Janičić, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS, vol. 6877, pp. 201-220. Springer, Heidelberg (2011) · Zbl 1252.68264 · doi:10.1007/978-3-642-25070-5_12
[29] Wernick, W.: Triangle constructions vith three located points. Math. Mag. 55(4), 227-230 (1982) · Zbl 0497.51016 · doi:10.2307/2690164
[30] Pambuccian, V.: Axiomatizing geometric constructions. J. Appl. Logic 6(1), 24-46 (2008) · Zbl 1143.03007 · doi:10.1016/j.jal.2007.02.001
[31] Beeson, M.: Logic of ruler and compass constructions. In: Cooper, S.B., Dawar, A., Löwe, B. (eds.) CiE 2012. LNCS, vol. 7318, pp. 46-55. Springer, Heidelberg (2012) · Zbl 1357.03093 · doi:10.1007/978-3-642-30870-3_6
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.