Automated theorem proving in GeoGebra: current achievements

DOI10.1007/s10817-015-9326-4zbMath1356.68181OpenAlexW2064030682MaRDI QIDQ286780

Zoltán Kovács, Francisco Botana, Simon Weitzhofer, Markus Hohenwarter, Predrag Janičić, Ivan Petrović, Tomás Recio

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10902/7265

zbMATH Keywords

automatic theorem provingintelligent tutoring systemsinteractive learning environmentssecondary education

Mathematics Subject Classification ID

Geometry education (97Gxx) Technological tools, calculators (aspects of mathematics education) (97U70)

Related Items

On the unavoidable uncertainty of truth in dynamic geometry proving, The Relation Tool in GeoGebra 5, Rewriting input expressions in complex algebraic geometry provers, Portfolio theorem proving and prover runtime prediction for geometry, Formalization of the arithmetization of Euclidean plane geometry and applications, Automated discovery of geometric theorems based on vector equations, Towards an Automated Geometer, Automatic Deduction in an AI Geometry Book, Detecting truth, just on parts, Can I bring my calculator to the exam? Some reflections on the abstraction level of computer algebra systems, Automated discovery of angle theorems, A program to create new geometry proof problems, Automated generation of illustrated proofs in geometry and beyond, Towards an intelligent and dynamic geometry book, Contemporary Interpretation of a Historical Locus Problem with the Use of Computer Algebra, Automated deduction and knowledge management in geometry, A symbolic dynamic geometry system using the analytical geometry method, Towards the Automatic Discovery of Theorems in GeoGebra, A mechanical geometer, Locus computation in dynamic geometry environment, New dynamics in dynamic geometry: dragging constructed points, Reasoning about linkages with dynamic geometry, Taxonomies of geometric problems, Development of automatic reasoning tools in GeoGebra

Uses Software

• CoCoA
• Epsilon
• GCLC
• Mathematica
• MMP/Geometer
• SINGULAR
• GEOTHER 1.1
• GeoGebra
• Geometer's Sketchpad
• GeoProof
• GeoThms
• SATzilla
• ActiveMath
• Giac
• OpenGeoProver
• gcl
• GEX
• GeoView
• JGEX
• Geometrix
• CHYPRE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The area method. A recapitulation
• Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
• The parallel numerical method of mechanical theorem proving
• Using Gröbner bases to reason about geometry problems
• Automated reasoning in geometry theorem proving with Prolog
• Automatic discovery of theorems in elementary geometry
• A graphical user interface for formal proofs in geometry
• Geometry constructions language
• Giac and GeoGebra – Improved Gröbner Basis Computations
• GeoThms — a Web System for Euclidean Constructive Geometry
• An Introduction to Java Geometry Expert
• Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method
• A note on syntactic symmetry and the manipulation of formal systems by machine
• An introduction to geometry expert
• Machine Proofs in Geometry
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Automated Deduction in Geometry
• Automated Deduction in Geometry
• Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles