Automated Deduction – CADE-20
From MaRDI portal
Publication:5394621
DOI10.1007/11532231zbMath1135.03329OpenAlexW2485416161MaRDI QIDQ5394621
No author found.
Publication date: 1 November 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11532231
Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)
Related Items
Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems, A heuristic prover for real inequalities, Extending a Resolution Prover for Inequalities on Elementary Functions, Proof synthesis and reflection for linear arithmetic, MetiTarski: An automatic theorem prover for real-valued special functions, Linear quantifier elimination, A revision of the proof of the Kepler conjecture, Coquelicot: a user-friendly library of real analysis for Coq, Real World Verification, Proof Assistant Decision Procedures for Formalizing Origami, Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL, Combined Decision Techniques for the Existential Theory of the Reals, MetiTarski: An Automatic Prover for the Elementary Functions, Combining Isabelle and QEPCAD-B in the Prover’s Palette, Formalization of Bernstein polynomials and applications to global optimization
Uses Software
