Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
The Coq Proof Assistant, http://coq.inria.fr/
Pearson, K.R., Jones, A., Morris, S.A.: Abstract Algebra and Famous Impossibilities. Springer, Heidelberg (1991)
Alperin, R.C.: A Mathematical Theory of Origami Constructions and Numbers. New York Journal of Mathematics 6, 119–133 (2000)
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)
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)
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)
Huzita, H.: Axiomatic Development of Origami Geometry. In: Proceedings of the First International Meeting of Origami Science and Technology, pp. 143–158 (1989)
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)
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)
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)
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)
Narboux, J.: A Graphical User Interface for Formal Proofs in Geometry. Journal of Automated Reasoning 39(2), 161–180 (2007)
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)
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)
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)
Wolfram, S.: The Mathematica Book, 5th edn. Wolfram Media (2003)
Wu, W.T.: Basic Principles of Mechanical Theorem Proving in Elementary Geometry. Journal of Automated Reasoning 2, 221–252 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ghourabi, F., Ida, T., Kasem, A. (2011). Proof Documents for Automated Origami Theorem Proving. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds) Automated Deduction in Geometry. ADG 2010. Lecture Notes in Computer Science(), vol 6877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25070-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-25070-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25069-9
Online ISBN: 978-3-642-25070-5
eBook Packages: Computer ScienceComputer Science (R0)