An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic

DOI10.1007/978-3-642-14203-1_33zbMath1291.03112OpenAlexW1582116296MaRDI 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

Mathematics Subject Classification ID

Related Items (14)

Preface: Special issue on interpolation ⋮ Proof tree preserving tree interpolation ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ The map equality domain ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ 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 ⋮ An interpolating sequent calculus for quantifier-free Presburger arithmetic ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ On Interpolation in Decision Procedures ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic ⋮ Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic

Uses Software

• Princess

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

This page was built for publication: An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic