Linear quantifier elimination
From MaRDI portal
Recommendations
Cites work
- A Decision Procedure for the First Order Theory of Real Addition with Order
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Applying Linear Quantifier Elimination
- Automated Deduction – CADE-20
- Complete integer decision procedures as derived rules in HOL
- Constructive Type Classes in Isabelle
- Formal proof - the four color theorem
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 3408928 (Why is no real title available?)
- scientific article; zbMATH DE number 3022422 (Why is no real title available?)
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Isabelle/HOL. A proof assistant for higher-order logic
- Linear Quantifier Elimination
- The complexity of linear problems in fields
- Theorem Proving in Higher Order Logics
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Verifying Mixed Real-Integer Quantifier Elimination
Cited in
(32)- Dines-Fourier-Motzkin quantifier elimination and an application of corresponding transfer principles over ordered fields
- Eliminating disjunctions of leads-to properties
- Head linear reduction and pure proof net extraction
- Introduction to ``Milestones in interactive theorem proving
- Eliminating disjunctions by disjunction elimination
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- A verified decision procedure for orders in Isabelle/HOL
- Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL
- Quantifier elimination for linear modular constraints
- Applying Linear Quantifier Elimination
- Formalizing constructive quantifier elimination in Agda
- Weak Integer Quantifier Elimination Beyond the Linear Case
- Linear Quantifier Elimination
- scientific article; zbMATH DE number 68156 (Why is no real title available?)
- SMT-based model checking for recursive programs
- Str\(\dotplus\)ve and integers
- A roadmap to decidability
- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Advances in Databases and Information Systems
- Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Linear quantifier elimination as an abstract decision procedure
- Formalized proof systems for propositional logic
- Hall's theorem for enumerable families of finite sets
- Verified Quadratic Virtual Substitution for Real Arithmetic
- The QSMA algorithm for quantifiers in SMT
- An introduction to the theory of linear integer arithmetic (invited paper)
- Verified Quadratic Virtual Substitution for Real Arithmetic
- An incremental algorithm for DLO quantifier elimination via constraint propagation
- Weak quantifier elimination for the full linear theory of the integers
- Proof synthesis and reflection for linear arithmetic
This page was built for publication: Linear quantifier elimination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q707743)
