A refutational approach to geometry theorem proving
From MaRDI portal
Publication:1124373
DOI10.1016/0004-3702(88)90050-1zbMath0678.68094OpenAlexW1969337365MaRDI QIDQ1124373
Publication date: 1988
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0004-3702(88)90050-1
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (20)
Automatic determination of envelopes and other derived curves within a graphic environment ⋮ Proof-checking Euclid ⋮ Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries ⋮ A bibliography of quantifier elimination for real closed fields ⋮ Computer-based manipulation of systems of equations in elasticity problems with Gröbner bases ⋮ Elimination procedures for mechanical theorem proving in geometry ⋮ A generalized Euclidean algorithm for geometry theorem proving ⋮ A quantifier-elimination based heuristic for automatically generating inductive assertions for programs ⋮ When Is a Formula a Loop Invariant? ⋮ Geometric reasoning with logic and algebra ⋮ Limits of theory sequences over algebraically closed fields and applications. ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ Using geometric rewrite rules for solving geometric problems symbolically ⋮ On the Need of Radical Ideals in Automatic Proving: A Theorem About Regular Polygons ⋮ On One Method of Proving Inequalities in Automated Way ⋮ Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch's trick ⋮ Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking ⋮ Geometric theorem proving by integrated logical and algebraic reasoning ⋮ A software tool for the investigation of plane loci ⋮ Application of Gröbner bases to problems of movement of a particle
Cites Work
- Non-commutative Gröbner bases in algebras of solvable type
- Refutational theorem proving using term-rewriting systems
- On the application of Buchberger's algorithm to automated geometry theorem proving
- Using Gröbner bases to reason about geometry problems
- Bounds for the degrees in the Nullstellensatz
- Automated reasoning in geometry theorem proving with Prolog
- Proving geometry theorems with rewrite rules
- Basic principles of mechanical theorem proving in elementary geometries
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Über B. Buchbergers Verfahren, Systeme algebraischer Gleichungen zu lösen
- Comments on the translation of my PhD thesis: ``An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
- An examination of the geometry theorem machine
- Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems
- A new decision method for elementary algebra
- Automated Theorem Proving: After 25 Years
- Cylindrical Algebraic Decomposition I: The Basic Algorithm
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A refutational approach to geometry theorem proving
