Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
From MaRDI portal
Publication:5387851
DOI10.1007/11591191_26zbMath1143.03334OpenAlexW1519123794MaRDI QIDQ5387851
Publication date: 27 May 2008
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11591191_26
Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30) Quantifier elimination, model completeness, and related topics (03C10)
Related Items
Semi-intelligible Isar proofs from machine-generated proofs ⋮ Proof synthesis and reflection for linear arithmetic ⋮ A mechanical verification of the stressing algorithm for negative cost cycle detection in networks ⋮ Linear quantifier elimination ⋮ Certified Reasoning with Infinity
