Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
From MaRDI portal
Publication:2354917
DOI10.1007/s10472-014-9443-5zbMath1327.68206OpenAlexW2148169424WikidataQ113904583 ScholiaQ113904583MaRDI QIDQ2354917
Sana Stojanović Đurđević, Predrag Janičić, Julien Narboux
Publication date: 27 July 2015
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01091011/file/AFTarski.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (9)
Finding proofs in Tarskian geometry ⋮ Learning to solve geometric construction problems from images ⋮ From informal to formal proofs in Euclidean geometry ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Proof-checking Euclid ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Tarski geometry axioms. IV: Right angle ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Tarski geometry axioms. III
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automated development of Tarski's geometry
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- A fully automatic theorem prover with human-style output
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Proof and Computation in Geometry
- From Tarski to Hilbert
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
- Automatic Proof and Disproof in Isabelle/HOL
- OTTER Proofs in Tarskian Geometry
- Skolem Machines and Geometric Logic
- Formalizing Hilbert’s Grundlagen in Isabelle/Isar
- Tarski's System of Geometry
- A Machine-Checked Proof of the Odd Order Theorem
- Communicating Formal Proofs: The Case of Flyspeck
- Automating Coherent Logic
- A further simplification of Tarski's axioms of geometry
- Mechanical Theorem Proving in Tarski’s Geometry
- Automated Deduction in Geometry
- A Vernacular for Coherent Logic
- A Machine-Oriented Logic Based on the Resolution Principle
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
This page was built for publication: Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
