Proof Documents for Automated Origami Theorem Proving

被引:0
|
作者
Ghourabi, Fadoua [1 ]
Ida, Tetsuo [1 ]
Kasem, Asem [2 ]
机构
[1] Univ Tsukuba, Dept Comp Sci, Tsukuba, Ibaraki 3058573, Japan
[2] Yarmouk Private Univ, Fac Informat & Commun Engn, Daraa, Syria
来源
关键词
CONSTRUCTION;
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:78 / +
页数:3
相关论文
共 50 条
  • [1] Proof simplification and automated theorem proving
    Kinyon, Michael
    [J]. PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 2019, 377 (2140):
  • [2] Proof procedures for an automated theorem-proving program
    Kim, SW
    Kim, SM
    [J]. KYBERNETES, 1998, 27 (8-9) : 1075 - +
  • [3] Morley's theorem revisited: Origami construction and automated proof
    Ida, Tetsuo
    Kasem, Asem
    Ghourabi, Fadoua
    Takahashi, Hidekazu
    [J]. JOURNAL OF SYMBOLIC COMPUTATION, 2011, 46 (05) : 571 - 583
  • [4] Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies
    Mo, Guangshuai
    Xiong, Yan
    Huang, Wenchao
    Ma, Lu
    [J]. 2020 6TH INTERNATIONAL CONFERENCE ON BIG DATA COMPUTING AND COMMUNICATIONS (BIGCOM 2020), 2020, : 71 - 75
  • [5] Automated theorem proving
    Li, HB
    [J]. GEOMETRIC ALGEBRA WITH APPLICATIONS IN SCIENCE AND ENGINEERING, 2001, : 110 - +
  • [6] Automated theorem proving
    Plaisted, David A.
    [J]. WILEY INTERDISCIPLINARY REVIEWS-COGNITIVE SCIENCE, 2014, 5 (02) : 115 - 128
  • [7] UNIT PROOF AND INPUT PROOF IN THEOREM PROVING
    CHANG, CL
    [J]. JOURNAL OF THE ACM, 1970, 17 (04) : 698 - &
  • [8] Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving
    Jacquel, Melanie
    Berkani, Karim
    Delahaye, David
    Dubois, Catherine
    [J]. SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 253 - +
  • [9] Verifying B proof rules using deep embedding and automated theorem proving
    Jacquel, Melanie
    Berkani, Karim
    Delahaye, David
    Dubois, Catherine
    [J]. SOFTWARE AND SYSTEMS MODELING, 2015, 14 (01): : 101 - 119
  • [10] Verifying B proof rules using deep embedding and automated theorem proving
    Mélanie Jacquel
    Karim Berkani
    David Delahaye
    Catherine Dubois
    [J]. Software & Systems Modeling, 2015, 14 : 101 - 119