Basic principles of mechanical theorem proving in elementary geometries
From MaRDI portal
Publication:1101257
DOI10.1007/BF02328447zbMath0642.68163MaRDI QIDQ1101257
Publication date: 1986
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Euclidean geometryalgebraic varietiesanalytic geometryautomatic theorem provingMorley's theorempolynomial divisionPascal-conic theoremreducible polynomialswell-ordering of polynomials
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
