Automated generation of illustrated proofs in geometry and beyond
From MaRDI portal
Publication:6185789
DOI10.1007/s10472-023-09857-yOpenAlexW4382982372MaRDI QIDQ6185789
Predrag Janičić, Julien Narboux
Publication date: 8 January 2024
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-023-09857-y
Knowledge representation (68T30) Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Software, source code, etc. for problems pertaining to geometry (51-04) Natural language processing (68T50)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automated theorem proving in GeoGebra: current achievements
- Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
- Visually dynamic presentation of proofs in plane geometry. II: Automated generation of visually dynamic presentations with the full-angle method and the deductive database method
- Theorem proving as constraint solving with coherent logic
- A graphical user interface for formal proofs in geometry
- Proof-checking Euclid
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Geometry constructions language
- GEOMETRISATION OF FIRST-ORDER LOGIC
- An Introduction to Java Geometry Expert
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs
- Automating Coherent Logic
- A Vernacular for Coherent Logic
- GCLC — A Tool for Constructive Euclidean Geometry and More Than That
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- Automated Deduction in Geometry
- Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles