Basic principles of mechanical theorem proving in elementary geometries

DOI10.1007/BF02328447zbMath0642.68163MaRDI QIDQ1101257

Publication date: 1986

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

Euclidean geometry algebraic varieties analytic geometry automatic theorem proving Morley's theorem polynomial division Pascal-conic theorem reducible polynomials well-ordering of polynomials

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Software, source code, etc. for problems pertaining to geometry (51-04) Analytic and descriptive geometry (51N99)

Related Items

Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm, Chordality Preserving Incremental Triangular Decomposition and Its Implementation, An algorithm for solving singular perturbation problems with mechanization, The computer searches for Pascal conics, Symmetry reductions, exact solutions, and conservation laws of the generalized Zakharov equations, Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries, The LaSalle's invariant sets for a class of Lotka-Volterra prey-predator chain systems, A New Method for Solving Polynomial Systems with Noise over $\mathbb{F}_2$ and Its Applications in Cold Boot Key Recovery, Computing final polynomials and final syzygies using Buchberger's Gröbner bases method, Deriving some new conditions on the existence of eight limit cycles for a cubic system, A bibliography of quantifier elimination for real closed fields, Generalizing Morley's and other theorems with automated realization, Ordering in mechanical geometry theorem proving, \textit{Theorema}: Towards computer-aided mathematical theory exploration, Polynomials root-finding using a SLEFE-based clipping method, Wu's method and its application to perspective viewing, Wu's characteristic set method for SystemVerilog assertions verification, An efficient algorithm for factoring polynomials over algebraic extension field, Computer aided proof for the global stability of Lotka-Volterra systems, A refutational approach to geometry theorem proving, A recursive algorithm for constructing complicated Dixon matrices, The dimension method in elementary and differential geometry, A category of geometric spaces: Some computational aspects, A quantifier-elimination based heuristic for automatically generating inductive assertions for programs, Automatic deduction in (dynamic) geometry: Loci computation, A strategy for speeding-up the computation of characteristic sets, A Direttissimo Algorithm for Equidimensional Decomposition, Analyzing the dual space of the saturated ideal of a regular set and the local multiplicities of its zeros, Bifurcation analysis and complex dynamics of a Kopel triopoly model, A signature-based algorithm for computing the nondegenerate locus of a polynomial system, Characteristic set algorithms for equation solving in finite fields, Decomposing polynomial sets into simple sets over finite fields: the zero-dimensional case, Automated discovery of angle theorems, A program to create new geometry proof problems, Morley's theorem revisited: origami construction and automated proof, Automated reducible geometric theorem proving and discovery by Gröbner basis method, A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications, Parametric equation solving and quantifier elimination in finite fields with the characteristic set method, On the efficiency of solving Boolean polynomial systems with the characteristic set method, Limits of theory sequences over algebraically closed fields and applications., Computing equilibria of semi-algebraic economies using triangular decomposition and real solution classification, Solving SAT by algorithm transform of Wu's method, A criterion for testing whether a difference ideal is prime, Ritt-Wu characteristic set method for Laurent partial differential polynomial systems, A survey on algorithms for computing comprehensive Gröbner systems and comprehensive Gröbner bases, Computing strong regular characteristic pairs with Gröbner bases, Mechanical manipulation for a class of differential systems, Computational Origami Construction as Constraint Solving and Rewriting, Attacking Bivium and Trivium with the Characteristic Set Method, GEOTHER: A geometry theorem prover, Irreducible decomposition of algebraic varieties via characteristic sets and Gröbner bases, Using geometric rewrite rules for solving geometric problems symbolically, On $n$-sectors of the angles of an arbitrary triangle, Computer algebra methods in the study of nonlinear differential systems, Elimination Techniques for Program Analysis, A systematic framework for solving geometric constraints analytically, A new algorithm for symbolic integration with application, Computing Switching Surfaces in Optimal Control Based on Triangular Decomposition, A mechanical algorithm for solving the Volterra integral equation, Mechanical algorithm for solving the second kind of Volterra integral equation, Computing the radical of an ideal in positive characteristic, A new algorithm for integral of trigonometric functions with mechanization, The Implementation and Complexity Analysis of the Branch Gröbner Bases Algorithm Over Boolean Polynomial Rings, Mechanically proving geometry theorems using a combination of Wu's method and Collins' method, Theorem proving by chain resolution, On the complexity of counting components of algebraic varieties, Proof Documents for Automated Origami Theorem Proving, Envelopes and offsets of two algebraic plane curves: exploration of their similarities and differences, An algorithm for solving DAEs with mechanization, On a Hybrid Symbolic-Connectionist Approach for Modeling the Kinematic Robot Map - and Benchmarks for Computer Algebra, Multiplicity-preserving triangular set decomposition of two polynomials, New exact solutions for three nonlinear evolution equations, Analyses and implementations of chordality-preserving top-down algorithms for triangular decomposition

Cites Work