Repository logo

Álgebra Computacional | Computational Algebra

Permanent URI for this community

http://hdl.handle.net/10400.2/15583

Browse

Browsing Álgebra Computacional | Computational Algebra by Author "Baeta, Nuno Miguel dos Santos"

Now showing 1 - 1 of 1
  • Working environment for automated deduction in geometry
    Publication . Baeta, Nuno Miguel dos Santos; Almeida, Pedro Henrique e Figueiredo Quaresma de
    Given its formal, logical and spatial properties, geometry is well suited to be used in teaching environments that include dynamic geometry systems (DGS), geometry automated theorem provers (GATP) and repositories of geometric problems. With the help of the DGS, students can build geometric constructions and conjecture about their properties. With the GATP, students may check the soundness of the constructions (e.g., if two given lines are parallel) and also create formal proofs of conjectures. These tools, backed by repositories of geometric knowledge, provide teachers and students with a framework supported by a large set of geometric constructions and conjectures, for the development of experiments.The ultimate goal is to contribute towards the development of a working environment, where the dynamic geometry component and the automated deduction component work together, providing proofs for plane geometry, in natural language and with a visually dynamic presentation. Quoting Gila Hanna “the best proof is one that also helps understand the meaning of the theorem being proved: to see not only that it is true, but also why it is true”.Building on the work already done in the open source project Open Geometry Prover (OGP), the initial goal was to complete the GATP based on the full-angle method, improving OGP’s library, and allowing the automated deduction in geometry community to profit from a new tool.The OGP project was originally developed by PhD student Ivan Petrović, under the guidance of Predrag Janičić of the University of Belgrade, Serbia, but it was not completed. Having taken over the project, now designated as the Open Geometry Prover Community Project (OGPCP), it was opted for a totally new implementation of a GATP based on the deductive databases for geometry method, having concluded a first version of the automatic theorem prover, the Geometry Deductive Database Prover, fully integrated in the OGPCP.
    2024-02-21Doctoral thesis Open access Show more