Linear quantifier elimination
From MaRDI portal
Publication:707743
DOI10.1007/s10817-010-9183-0zbMath1207.68339OpenAlexW1971038681WikidataQ56059277 ScholiaQ56059277MaRDI QIDQ707743
Publication date: 8 October 2010
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9183-0
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Introduction to ``Milestones in interactive theorem proving ⋮ Hall's theorem for enumerable families of finite sets ⋮ Unnamed Item ⋮ Unnamed Item ⋮ SMT-based model checking for recursive programs ⋮ A Roadmap to Decidability
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The complexity of linear problems in fields
- Isabelle/HOL. A proof assistant for higher-order logic
- Applying Linear Quantifier Elimination
- Linear Quantifier Elimination
- Complete Integer Decision Procedures as Derived Rules in HOL
- Constructive Type Classes in Isabelle
- Verifying Mixed Real-Integer Quantifier Elimination
- A Decision Procedure for the First Order Theory of Real Addition with Order
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
This page was built for publication: Linear quantifier elimination
