Showing 1–2 of 2 results for author: Šukilović, T

Towards Automated Readable Proofs of Ruler and Compass Constructions

Authors: Vesna Marinković, Tijana Šukilović, Filip Marić

Abstract: Although there are several systems that successfully generate construction steps for ruler and compass construction problems, none of them provides readable synthetic correctness proofs for generated constructions. In the present work, we demonstrate how our triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic so that it gener… ▽ More Although there are several systems that successfully generate construction steps for ruler and compass construction problems, none of them provides readable synthetic correctness proofs for generated constructions. In the present work, we demonstrate how our triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic so that it generates construction correctness proofs, that are both human-readable and formal (can be checked by interactive theorem provers such as Coq or Isabelle/HOL). These proofs currently rely on many high-level lemmas and our goal is to have them all formally shown from the basic axioms of geometry. △ Less

Submitted 22 January, 2024; originally announced January 2024.

Comments: In Proceedings ADG 2023, arXiv:2401.10725

ACM Class: F.4.1

Journal ref: EPTCS 398, 2024, pp. 11-20

On Automating Triangle Constructions in Absolute and Hyperbolic Geometry

Authors: Vesna Marinković, Tijana Šukilović, Filip Marić

Abstract: We describe first steps towards a system for automated triangle constructions in absolute and hyperbolic geometry. We discuss key differences between constructions in Euclidean, absolute and hyperbolic geometry, compile a list of primitive constructions and lemmas used for constructions in absolute and hyperbolic geometry, build an automated system for solving construction problems and test it on… ▽ More We describe first steps towards a system for automated triangle constructions in absolute and hyperbolic geometry. We discuss key differences between constructions in Euclidean, absolute and hyperbolic geometry, compile a list of primitive constructions and lemmas used for constructions in absolute and hyperbolic geometry, build an automated system for solving construction problems and test it on a corpus of triangle-construction problems. We also provide an online compendium containing construction descriptions and illustrations. △ Less

Submitted 3 January, 2022; originally announced January 2022.

Comments: In Proceedings ADG 2021, arXiv:2112.14770

ACM Class: I.2.3

Journal ref: EPTCS 352, 2021, pp. 14-26