Finding proofs in Tarskian geometry

DOI10.1007/S10817-016-9392-2zbMath1414.68100arXiv1606.07095OpenAlexW2963109403WikidataQ113901246 ScholiaQ113901246MaRDI QIDQ2362499

Larry Wos, Michael J. Beeson

Publication date: 10 July 2017

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

Full work available at URL: https://arxiv.org/abs/1606.07095

zbMATH Keywords

theorem provingautomated deductionTarskian geometry

Mathematics Subject Classification ID

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

Related Items (8)

Learning to solve geometric construction problems from images ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Euclid after Computer Proof-Checking ⋮ Brouwer and Euclid ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Larry Wos: visions of automated reasoning

Uses Software

• Unnamed Item
• Sledgehammer
• Flyspeck

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• A synthetic proof of Pappus' theorem in Tarski's geometry
• From Tarski to Hilbert
• OTTER Proofs in Tarskian Geometry
• Tarski's System of Geometry
• Hammering towards QED
• A Fascinating Country in the World of Computing

This page was built for publication: Finding proofs in Tarskian geometry