Linear quantifier elimination

DOI10.1007/s10817-010-9183-0zbMath1207.68339OpenAlexW1971038681WikidataQ56059277 ScholiaQ56059277MaRDI QIDQ707743

Tobias Nipkow

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

zbMATH Keywords

verificationquantifier eliminationlinear arithmetic

Mathematics Subject Classification ID

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

• Isabelle/HOL

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