×

Proof documents for automated origami theorem proving. (English) Zbl 1350.68235

Schreck, Pascal (ed.) et al., Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22–24, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-25069-9/pbk). Lecture Notes in Computer Science 6877. Lecture Notes in Artificial Intelligence, 78-97 (2011).
Summary: A proof document for origami theorem proving is a record of entire process of reasoning about origami construction and theorem proving. It is produced at the completion of origami theorem proving as a kind of proof certificate. It describes in detail how the whole process of an origami construction and the subsequent theorem proving are carried out in our computational origami system. In particular, it describes logical and algebraic transformations of the prescription of origami construction into mathematical models that in turn become amenable to computation and verification. The structure of the proof document is detailed using an illustrative example that reveals the importance of such a document in the analysis of origami construction and theorem proving.
For the entire collection see [Zbl 1227.68009].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
51M15 Geometric constructions in real or complex geometry
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] The Coq Proof Assistant, http://coq.inria.fr/ · Zbl 1465.03051
[2] Pearson, K.R., Jones, A., Morris, S.A.: Abstract Algebra and Famous Impossibilities. Springer, Heidelberg (1991) · Zbl 0758.12001
[3] Alperin, R.C.: A Mathematical Theory of Origami Constructions and Numbers. New York Journal of Mathematics 6, 119–133 (2000) · Zbl 1065.51501
[4] Buchberger, B., Dupre, C., Jebelean, T., Kriftner, F., Nakagawa, K., Văsaru, D., Windsteiger, W.: The Theorema Project: A Progress Report. In: Symbolic Computation and Automated Reasoning (Calculemus 2000), St. Andrews, Scotland, pp. 98–113 (2000) · Zbl 1017.68110
[5] Ghourabi, F., Ida, T.: Orikoto: A Language for Origami Construction and Theorem Proving. In: Frontiers of Computer Science in China (2010); (Submitted, the extended abstract was presented in the fifth International Conference on Origami in Science, Mathematics and Education (5OSME)
[6] Ghourabi, F., Ida, T., Takahashi, H., Marin, M., Kasem, A.: Logical and Algebraic View of Huzita’s Origami Axioms with Applications to Computational Origami. In: Proceedings of the 22nd ACM Symposium on Applied Computing (SAC 2007), Seoul, Korea, pp. 767–772 (2007) · doi:10.1145/1244002.1244173
[7] Huzita, H.: Axiomatic Development of Origami Geometry. In: Proceedings of the First International Meeting of Origami Science and Technology, pp. 143–158 (1989)
[8] Ida, T., Kasem, A., Ghourabi, F., Takahashi, H.: Morley’s theorem revisited: Origami construction and automated proof. Journal of Symbolic Computation 46(5), 571–583 (2011) · Zbl 1211.51011 · doi:10.1016/j.jsc.2010.10.007
[9] Ida, T., Takahashi, H., Marin, M., Ghourabi, F., Kasem, A.: Computational Construction of a Maximum Equilateral Triangle Inscribed in an Origami. In: Iglesias, A., Takayama, N. (eds.) ICMS 2006. LNCS, vol. 4151, pp. 361–372. Springer, Heidelberg (2006) · Zbl 1230.51023 · doi:10.1007/11832225_36
[10] Justin, J.: Résolution par le pliage de l’équation du troisième degré et applications géométriques. In: Proceedings of the First International Meeting of Origami Science and Technology, pp. 251–261 (1989)
[11] Kasem, A., Ghourabi, F., Ida, T.: Origami Axioms and Circle Extension. In: Proceedings of the 26th Symposium on Applied Computing, pp. 1106–1111. ACM press (2011) · Zbl 1350.68235 · doi:10.1145/1982185.1982429
[12] Narboux, J.: A Graphical User Interface for Formal Proofs in Geometry. Journal of Automated Reasoning 39(2), 161–180 (2007) · Zbl 1131.68094 · doi:10.1007/s10817-007-9071-4
[13] Robu, J., Ida, T., Ţepeneu, D., Takahashi, H., Buchberger, B.: Computational Origami Construction of a Regular Heptagon with Automated Proof of Its Correctness. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol. 3763, pp. 19–33. Springer, Heidelberg (2006) · Zbl 1159.68558 · doi:10.1007/11615798_2
[14] Wang, D.: GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol. 2930, pp. 194–215. Springer, Heidelberg (2004) · Zbl 1202.68390 · doi:10.1007/978-3-540-24616-9_12
[15] Wantzel, P.L.: Recherches sur les moyens de connaitre si un problème de géométrie peut se résoudre avec la règle et le compas. Journal de Mathématiques Pures et Appliquées, 366–372 (1984)
[16] Wolfram, S.: The Mathematica Book, 5th edn. Wolfram Media (2003)
[17] Wu, W.T.: Basic Principles of Mechanical Theorem Proving in Elementary Geometry. Journal of Automated Reasoning 2, 221–252 (1986) · Zbl 0642.68163 · doi:10.1007/BF02328447
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.