Abstract

BibTeX

@InProceedings{10.1007/978-3-030-52200-1_26,
  author="Ol{\v{s}}{\'a}k, Miroslav",
  editor="Bigatti, Anna Maria
  and Carette, Jacques
  and Davenport, James H.
  and Joswig, Michael
  and de Wolff, Timo",
  title="GeoLogic -- Graphical Interactive Theorem Prover for Euclidean Geometry",
  booktitle="Mathematical Software -- ICMS 2020",
  year="2020",
  publisher="Springer International Publishing",
  address="Cham",
  pages="263--271",
  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.",
  isbn="978-3-030-52200-1"
}