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
Symbolic computation and algebraic computation (68W30) Special varieties (14M99) Projective and enumerative algebraic geometry (14N99)
Related Items
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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
