GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry

DOI10.1007/978-3-030-52200-1_26MaRDI QIDQ5041061zbMATH OpenOpenAlexFDO

Publication date 13 October 2022

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mechanization of proofs and logical operations (03B35) Elementary problems in Euclidean geometries (51M04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: Domain of mathematical logic in computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both of these are hard to access by AI from the human-imitation approach: ATPs often use human-unfriendly logical foundations while ITPs are meant for formalizing existing proofs rather than problem solving. We aim to create a simple human-friendly logical system for mathematical problem solving. We picked the case study of Euclidean geometry as it can be easily visualized, has simple logic, and yet potentially offers many high-school problems of various difficulty levels. To make the environment user friendly, we abandoned strict logic required by ITPs, allowing to infer topological facts from pictures. We present our system for Euclidean geometry, together with a graphical application GeoLogic, similar to GeoGebra, which allows users to interactively study and prove properties about the geometrical setup.

Recommendations

Cites work

Cited in

(7)

Describes a project that uses

Uses Software

This page was built for publication: GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry

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