×

zbMATH — the first resource for mathematics

Proof assistant decision procedures for formalizing origami. (English) Zbl 1335.68230
Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 45-57 (2011).
Summary: Origami constructions have interesting properties that are not covered by standard euclidean geometry. Such properties have been shown with the help of computer algebra systems. Proofs performed with computer algebra systems can be accompanied by proof documents, still they lack complete mathematical rigorousity, like the one provided by proof assistant checked proofs. Transforming such proofs to machine checkable proof scripts poses a number of challenges.
In this paper we describe issues that arise when proving properties of origami constructions using proof assistant decision procedures. We examine the strength of Gröbner Bases implementations comparing proof assistants with each other and with the implementations provided in computer algebra systems. We show ad-hoc decision procedures that can be used to optimize the proofs. We show how maximum equilateral triangle inscribed in a square construction can be formalized. We show how a equation system solving mechanism can be embedded in a CAS decision procedure of a proof assistant.
For the entire collection see [Zbl 1218.68014].
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., Owre, S.: Computer algebra meets automated theorem proving: Integrating Maple and PVS. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 27–42. Springer, Heidelberg (2001) · Zbl 1005.68997 · doi:10.1007/3-540-44755-5_4
[2] Aslaksen, H.: Multiple-valued complex functions and computer algebra. SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic Manipulation) 30(2), 12–20 (1996) · Zbl 1097.30500
[3] Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliâtre, J.C., Giménez, E., Herbelin, H., et al.: The Coq Proof Assistant Reference Manual Version 8.3. LogiCal project (2010), http://coq.inria.fr/refman/
[4] Cohen, C., Mahboubi, A.: A formal quantifier elimination for algebraically closed fields. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 189–203. Springer, Heidelberg (2010) · Zbl 1286.68394 · doi:10.1007/978-3-642-14128-7_17
[5] Ghourabi, F., Ida, T., Kasem, A.: Proof documents for automated origami theorem proving. Submitted to ADG 2011 post-proceedings (2011) · Zbl 1350.68235
[6] Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996) · doi:10.1007/BFb0031814
[7] Huzita, H.: Axiomatic development of origami geometry. In: Huzita, H. (ed.) Proceedings of the First International Meeting of Origami Science and Technology, pp. 143–158 (1989)
[8] Huzita, H.: The trisection of a given angle solved by the geometry of origami. In: Huzita, H. (ed.) Proceedings of the First International Meeting of Origami Science and Technology, pp. 195–214 (1989)
[9] Ida, T., Ghourabi, F., Kasem, A., Kaliszyk, C.: Towards theory of origami fold. Submitted to ISSAC (2011) · Zbl 1350.68235
[10] Janicic, P.: Geometry constructions language. J. Autom. Reasoning 44(1-2), 3–24 (2010) · Zbl 1185.68626 · doi:10.1007/s10817-009-9135-8
[11] Justin, J.: Résolution par le pliage de l’équation du troisième degré et applications géométriques. In: Huzita, H. (ed.) Proceedings of the First International Meeting of Origami Science and Technology, pp. 251–261 (1989)
[12] Kaliszyk, C.: Prototype computer algebra system in HOL Light, http://score.cs.tsukuba.ac.jp/ kaliszyk/holcas.php
[13] Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 94–105. Springer, Heidelberg (2007) · Zbl 1202.68382 · doi:10.1007/978-3-540-73086-6_8
[14] Kasem, A., Ida, T.: Computational origami environment on the Web. Frontiers of Computer Science in China 2(1), 39–54 (2008) · doi:10.1007/s11704-008-0009-8
[15] Kasem, A., Ida, T., Takahashi, H., Marin, M., Ghourabi, F.: E-origami system Eos. In: Proceedings of the Annual Symposium of Japan Society for Software Science and Technology, JSSST, Tokyo, Japan (September 2006) · Zbl 1230.51023
[16] McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 295–314. Springer, Heidelberg (2005) · Zbl 1135.03329 · doi:10.1007/11532231_22
[17] Medina-Bulo, I., Palomo-Lozano, F., Ruiz-Reina, J.-L.: A verified Common Lisp implementation of Buchberger’s algorithm in ACL2. J. Symb. Comput. 45(1), 96–123 (2010) · Zbl 1194.68155 · doi:10.1016/j.jsc.2009.07.002
[18] Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reasoning 39(2), 161–180 (2007) · Zbl 1131.68094 · doi:10.1007/s10817-007-9071-4
[19] Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
[20] Pottier, L.: Connecting Gröbner bases programs with Coq to do proofs in algebra, geometry and arithmetics. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR Workshops. CEUR Workshop Proceedings, vol. 418, CEUR-WS.org (2008)
[21] Critique of the Mathematical Abilities of CA Systems. In: Wester, M. (ed.) Contents of Computer Algebra Systems: A Practical Guide, John Wiley & Sons, Chichester (1999)
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.