Linear Quantifier Elimination

DOI10.1007/978-3-540-71070-7_3MaRDI QIDQ3541684zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow

Publication date 27 November 2008

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71070-7_3

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Linear quantifier elimination
• Verifying Mixed Real-Integer Quantifier Elimination
• Linear quantifier elimination as an abstract decision procedure
• Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL
• A verified decision procedure for orders in Isabelle/HOL

Cited in

(29)

• Dines-Fourier-Motzkin quantifier elimination and an application of corresponding transfer principles over ordered fields
• Head linear reduction and pure proof net extraction
• Solving quantified linear arithmetic by counterexample-guided instantiation
• 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
• A layered algorithm for quantifier elimination from linear modular constraints
• Applying Linear Quantifier Elimination
• Formalizing the Logic-Automaton Connection
• Formalizing constructive quantifier elimination in Agda
• scientific article; zbMATH DE number 68156 (Why is no real title available?)
• SMT solving for functional programming over infinite structures
• Real World Verification
• Str\(\dotplus\)ve and integers
• 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
• Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
• FMplex: a novel method for solving linear real arithmetic problems
• FMplex: exploring a bridge between Fourier-Motzkin and simplex
• Linear quantifier elimination
• On the normal forms and computational power of virus machines
• 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

Describes a project that uses

Uses Software

• 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 Q3541684)