OTTER Proofs in Tarskian Geometry

DOI10.1007/978-3-319-08587-6_38zbMath1414.68099OpenAlexW2275018860MaRDI QIDQ3192214

Larry Wos, Michael J. Beeson

Publication date: 26 September 2014

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08587-6_38

zbMATH Keywords

Tarskian geometry

Mathematics Subject Classification ID

General theory of distance geometry (51K05) Euclidean geometries (general) and generalizations (51M05)

Related Items

Finding proofs in Tarskian geometry ⋮ Implementing Euclid's straightedge and compass constructions in type theory ⋮ System Description: E.T. 0.1 ⋮ Tarski geometry axioms. IV: Right angle ⋮ Retrieving geometric information from images: the case of hand-drawn diagrams ⋮ Tarski geometry axioms. III ⋮ Larry Wos: visions of automated reasoning ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• Coq
• OTTER