Formalization of origami and origami-programming based on algebraic graph rewriting

对纸的折纸进行抽象，建立折纸的形式化理论是我们的最终目标。为此，我们用代数图改写理论形式化了折纸，并验证了折纸的某些几何性质。研究结果如下：(1)开发了一种折纸图形改写语言及其解释器。(2)为了使图形改写具体化，以用于模拟实际折纸和验证几何性质，我们开发了将基本折叠转换为代数表达式的算法。(3)在上述发展的同时，我们扩展和改进了我们开发的电子折纸系统Eos。扩展使我们能够自动验证更多的几何定理，并加快了证明的计算速度。

Abstraction of paper fold (origami) and establishment of a formal theory of fold are our ultimate goal. Towards that goal, we formalized origami by algebraic graph rewriting theory and verified certain geometrical propertiesof origami. The results we obtained are as follows:(1) We develop a graph rewriting language for origami and its interpreter.(2) In order to concretize the graph rewriting to be used to simulate actual origami and to verify geometrical properties, we developed algorithms for transformingbasic folds to algebraic expressions.(3) In parallel with the above developments we extended and improved e-origami system Eos that we have developed. The extension enables us to automatically verify more geometrical theorems and to speed up the computation of proving.