A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools

• URL: http://arxiv.org/abs/2303.05863v1
• Date: Fri, 10 Mar 2023 11:36:10 GMT
• Title: A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools
• Authors: Joana Teles (CMUC / Department of Mathematics, University of Coimbra), Vanda Santos (CIDTFF, University of Aveiro and CISUC), Pedro Quaresma (CISUC / Department of Mathematics, University of Coimbra)
• Abstract summary: The introduction of automated deduction systems in secondary schools face several bottlenecks. The dissonance between the outcomes of the geometry automated theorem provers and the normal practice of conjecturing and proving in schools is a major barrier to a wider use of such tools in an educational environment. A lesson plan is presented, its goal is the introduction of formal demonstration of proving geometric theorems, trying to motivate students to that goal.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The introduction of automated deduction systems in secondary schools face several bottlenecks. Beyond the problems related with the curricula and the teachers, the dissonance between the outcomes of the geometry automated theorem provers and the normal practice of conjecturing and proving in schools is a major barrier to a wider use of such tools in an educational environment. Since the early implementations of geometry automated theorem provers, applications of artificial intelligence methods, synthetic provers based on inference rules and using forward chaining reasoning are considered to be more suited for education proposes. Choosing an appropriate set of rules and an automated method that can use those rules is a major challenge. We discuss one such rule set and its implementation using the geometry deductive databases method (GDDM). The approach is tested using some chosen geometric conjectures that could be the goal of a 7th year class (approx. 12-year-old students). A lesson plan is presented, its goal is the introduction of formal demonstration of proving geometric theorems, trying to motivate students to that goal

Related papers

• Fuse, Reason and Verify: Geometry Problem Solving with Parsed Clauses from Diagram [78.79651421493058]
  We propose a neural-symbolic model for plane geometry problem solving (PGPS) with three key steps: modal fusion, reasoning process and knowledge verification. For reasoning, we design an explicable solution program to describe the geometric reasoning process, and employ a self-limited decoder to generate solution program autoregressively. We also construct a large-scale geometry problem dataset called PGPS9K, containing fine-grained annotations of textual clauses, solution program and involved knowledge solvers.
  arXiv  Detail & Related papers  (2024-07-10T02:45:22Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• Learning to Solve Geometry Problems via Simulating Human Dual-Reasoning Process [84.49427910920008]
  Geometry Problem Solving (GPS) has attracted much attention in recent years. It requires a solver to comprehensively understand both text and diagram, master essential geometry knowledge, and appropriately apply it in reasoning. Existing works follow a paradigm of neural machine translation and only focus on enhancing the capability of encoders, which neglects the essential characteristics of human geometry reasoning.
  arXiv  Detail & Related papers  (2024-05-10T03:53:49Z)
• Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving [0.0]
  We propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof.
  arXiv  Detail & Related papers  (2024-01-22T12:49:08Z)
• Open Geometry Prover Community Project [0.0]
  The Open Geometry Prover Community Project aims at the integration of the different efforts for the development of geometry automated theorem provers, under a common "umbrella" This article describes the necessary steps to such integration and the current implementation of some of those steps.
  arXiv  Detail & Related papers  (2022-01-03T09:27:23Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  We construct a new large-scale benchmark, Geometry3K, consisting of 3,002 geometry problems with dense annotation in formal language. We propose a novel geometry solving approach with formal language and symbolic reasoning, called Interpretable Geometry Problem solver (Inter-GPS) Inter-GPS incorporates theorem knowledge as conditional rules and performs symbolic reasoning step by step.
  arXiv  Detail & Related papers  (2021-05-10T07:46:55Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)
• Towards a Geometry Automated Provers Competition [0.0]
  A competition between GATP would allow to create a test bench for GATP developers to improve the existing ones and to propose new ones. It would also allow to establish a ranking for GATP that could be used by "clients" (e.g. developers of educational e-learning systems) to choose the best implementation for a given intended use.
  arXiv  Detail & Related papers  (2020-02-28T05:24:29Z)
• Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context [0.0]
  We present the core ideas we used to implement such a prover, from its encoding in Prolog to the generation of the complete set of proofs. We also present the main issues we encountered, as well as the chosen solutions.
  arXiv  Detail & Related papers  (2020-02-28T05:23:16Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.