Linear quantifier elimination
From MaRDI portal
Recommendations
Cites work
- 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?)
- 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
- 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 Mixed Real-Integer Quantifier Elimination
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
Cited in
(29)- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- scientific article; zbMATH DE number 7447763 (Why is no real title available?)
- Introduction to ``Milestones in interactive theorem proving
- A roadmap to decidability
- Head linear reduction and pure proof net extraction
- Verified Quadratic Virtual Substitution for Real Arithmetic
- scientific article; zbMATH DE number 68156 (Why is no real title available?)
- Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL
- Eliminating disjunctions of leads-to properties
- An incremental algorithm for DLO quantifier elimination via constraint propagation
- Linear quantifier elimination as an abstract decision procedure
- Weak Integer Quantifier Elimination Beyond the Linear Case
- Applying Linear Quantifier Elimination
- Linear Quantifier Elimination
- Dines-Fourier-Motzkin quantifier elimination and an application of corresponding transfer principles over ordered fields
- Str\(\dotplus\)ve and integers
- Hall's theorem for enumerable families of finite sets
- Weak quantifier elimination for the full linear theory of the integers
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- SMT-based model checking for recursive programs
- Advances in Databases and Information Systems
- Formalized proof systems for propositional logic
- Proof synthesis and reflection for linear arithmetic
- A verified decision procedure for orders in Isabelle/HOL
- Quantifier elimination for linear modular constraints
- Eliminating disjunctions by disjunction elimination
- Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL
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)
