A complete algorithm for automated discovering of a class of inequality-type theorems

DOI10.1007/BF02713938zbMath1125.68406MaRDI QIDQ865930

Xiaorong Hou, Lu Yang, Bican Xia

Publication date: 20 February 2007

Published in: Science in China. Series F (Search for Journal in Brave)

zbMATH Keywords

discriminant sequence; partial cylindrical algebraic decomposition; WR algorithm; Wu's elimination

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03C10: Quantifier elimination, model completeness, and related topics

Related Items

DISCOVERER, Recent advances in program verification through computer algebra, Modular composition modulo triangular sets and applications, Algorithms for computing triangular decomposition of polynomial systems, Some geometric properties of successive difference substitutions, Computing equilibria of semi-algebraic economies using triangular decomposition and real solution classification, Gröbner bases for polynomial systems with parameters, Solving parametric piecewise polynomial systems, Generic regular decompositions for parametric polynomial systems, Real zeros of the zero-dimensional parametric piecewise algebraic variety, An algorithm for isolating the real solutions of semi-algebraic systems, Special algorithm for stability analysis of multistable biological regulatory systems, Discovering polynomial Lyapunov functions for continuous dynamical systems, A review and prospect of readable machine proofs for geometry theorems, Solution to the generalized champagne problem on simultaneous stabilization of linear systems, A class of mechanically decidable problems beyond Tarski's model

Uses Software

• Maple

Cites Work

• Unnamed Item
• A complete discrimination system for polynomials
• Zeros and factors of polynomials with positive coefficients and protein- ligand binding
• A complete discrimination system for polynomials with complex coefficients and its automatic generation
• Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
• Recent advances on determining the number of real roots of parametric polynomials
• Complete characterization of strictly positive real regions and robust strictly positive real synthesis method
• Polynomial algorithms in computer algebra
• Which Triangles are Plane Sections of Regular Tetrahedra?
• Cylindrical Algebraic Decomposition I: The Basic Algorithm