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

基于代数图重写的折纸形式化和折纸编程

• 批准号: 22650001
• 负责人: IDA Tetsuo
• 金额: $ 2.1万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Challenging Exploratory Research
• 财政年份: 2010
• 资助国家: 日本
• 起止时间: 2010 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22650001/
• 关键词: 計算折紙論; 記号計算; 書換え系; 自動幾何定理証明; 制約問題; 代数的グラフ書換系; グロブナ基底計算; 計算折紙; グラフ書き換え; 検証支援系; 制約計算; 計算理論; グラフ書換系; 折紙計算論; 定理自動証明

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.

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

项目成果

Origami axioms and circle extension

• DOI: 10.1145/1982185.1982429
• 发表时间: 2011-03
• 期刊: Proceedings of the 2011 ACM Symposium on Applied Computing
• 作者: Asem Kasem;Fadoua Ghourabi;T. Ida

Eos Project

EOS项目

Morley's theorem revisited: Origami construction and automated proof

• DOI: 10.1016/j.jsc.2010.10.007
• 发表时间: 2011-05
• 期刊: J. Symb. Comput.
• 作者: T. Ida;Asem Kasem;Fadoua Ghourabi;Hidekazu Takahashi