A graphical user interface for formal proofs in geometry
From MaRDI portal
Publication:2462636
DOI10.1007/s10817-007-9071-4zbMath1131.68094MaRDI 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
Geometry; Interface; Coq; Automated theorem proving; Dynamic geometry; Proof assistant; Theorem prover
Related Items
Mechanical Theorem Proving in Tarski’s Geometry, A FORMAL SYSTEM FOR EUCLID’SELEMENTS, GeoProof, Geometry constructions language
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