Proof Assistant Decision Procedures for Formalizing Origami

DOI10.1007/978-3-642-22673-1_4zbMath1335.68230OpenAlexW57316377WikidataQ108482187 ScholiaQ108482187MaRDI QIDQ5200107

Tetsuo Ida, Cezary Kaliszyk

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22673-1_4

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Uses Software

• ACL2
• Coq
• GCLC
• Isabelle/HOL
• PVS
• GeoProof
• HOL Light
• gcl

Cites Work

• Unnamed Item
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• A graphical user interface for formal proofs in geometry
• Geometry constructions language
• Proof Documents for Automated Origami Theorem Proving
• A Formal Quantifier Elimination for Algebraically Closed Fields
• Multiple-valued complex functions and computer algebra
• Automated Deduction – CADE-20
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• Computational Construction of a Maximum Equilateral Triangle Inscribed in an Origami