An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
From MaRDI portal
Publication:5747778
DOI10.1007/978-3-642-14203-1_33zbMath1291.03112MaRDI QIDQ5747778
Thomas Wahl, Angelo Brillout, Philipp Rümmer, Daniel Kroening
Publication date: 14 September 2010
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_33
03B35: Mechanization of proofs and logical operations
03F30: First-order arithmetic and fragments
03C40: Interpolation, preservation, definability
Related Items
Quantifier-free interpolation in combinations of equality interpolating theories, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, Preface: Special issue on interpolation, Proof tree preserving tree interpolation, Interpolation systems for ground proofs in automated deduction: a survey, Guiding Craig interpolation with domain-specific abstractions, An interpolating sequent calculus for quantifier-free Presburger arithmetic, An extension of lazy abstraction with interpolation for programs with arrays, The map equality domain, On Interpolation in Decision Procedures, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints, SAT-Based Model Checking, Interpolation and Model Checking
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- An interpolating theorem prover
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
- Interpolants for Linear Arithmetic in SMT
- Polynomial Algorithms for Computing the Smith and Hermite Normal Forms of an Integer Matrix
- Interpolant Generation for UTVPI
- Constraint Solving for Interpolation
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Lazy Abstraction with Interpolants
