A refutational approach to geometry theorem proving

DOI10.1016/0004-3702(88)90050-1zbMath0678.68094OpenAlexW1969337365MaRDI QIDQ1124373

Deepak Kapur

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

zbMATH Keywords

Gröbner basissatisfiabilityNullstellensatz

Mathematics Subject Classification ID

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