A graphical user interface for formal proofs in geometry
From MaRDI portal
Publication:2462636
DOI10.1007/s10817-007-9071-4zbMath1131.68094OpenAlexW2088823840MaRDI QIDQ2462636
Publication date: 3 December 2007
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00118903/file/JARuitp-narboux.pdf
Related Items
GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry, Automated theorem proving in GeoGebra: current achievements, The Relation Tool in GeoGebra 5, Geometry constructions language, Automatic Deduction in an AI Geometry Book, Automated generation of illustrated proofs in geometry and beyond, Towards an intelligent and dynamic geometry book, The area method. A recapitulation, A review and prospect of readable machine proofs for geometry theorems, Automated deduction and knowledge management in geometry, A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs, Proof Assistant Decision Procedures for Formalizing Origami, Mechanical Theorem Proving in Tarski’s Geometry, GeoProof, Formalization of Wu’s Simple Method in Coq, Proof Documents for Automated Origami Theorem Proving, Thousands of Geometric Problems for Geometric Theorem Provers (TGTP), A FORMAL SYSTEM FOR EUCLID’SELEMENTS, Taxonomies of geometric problems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Formalizing Hilbert’s Grundlagen in Isabelle/Isar
- Term Rewriting and All That
- Machine Proofs in Geometry
- Automated Reasoning
- A Framework for Interactive Proof
- Mechanical Theorem Proving in Tarski’s Geometry
- Theorem Proving in Higher Order Logics
- Automated Deduction in Geometry
- Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
