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 (15)
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
This page was built for publication: Automated Deduction – CADE-20
