Linear Quantifier Elimination

DOI10.1007/978-3-540-71070-7_3zbMath1165.68465OpenAlexW1899861754MaRDI QIDQ3541684

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)

Related Items

A layered algorithm for quantifier elimination from linear modular constraints ⋮ A verified decision procedure for orders in Isabelle/HOL ⋮ Formalizing the Logic-Automaton Connection ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Unnamed Item ⋮ Linear quantifier elimination ⋮ Linear Quantifier Elimination as an Abstract Decision Procedure ⋮ Real World Verification

Uses Software

• Isabelle/HOL