Readable automated proofs of ruler and compass constructions

DOI10.1007/S10472-025-09971-ZMaRDI QIDQ6872776zbMATH OpenFDO

Authors Vesna Marinkovic, Tijana Šukilović, Viktor Novaković, Filip Marić

Publication date 19 January 2026

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/S10472-025-09971-Z

zbMATH Keywords

automated theorem provingcoherent logictriangle construction problems

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Computational methods for problems pertaining to geometry (51-08) Elementary problems in Euclidean geometries (51M04) Geometric constructions in real or complex geometry (51M15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A coherent logic based geometry theorem prover capable of producing formal and readable proofs
• An extension of triangle constructions from located points
• Automated generation of illustrations for synthetic geometry proofs
• Automated triangle constructions in hyperbolic geometry
• Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
• GCLC -- a tool for constructive Euclidean geometry and more than that
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 3586510 (Why is no real title available?)
• The area method. A recapitulation
• Theorem proving as constraint solving with coherent logic
• Triangle Constructions with Three Located Points

This page was built for publication: Readable automated proofs of ruler and compass constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6872776)