An interpolating sequent calculus for quantifier-free Presburger arithmetic

DOI10.1007/S10817-011-9237-YMaRDI QIDQ438556zbMATH OpenOpenAlexFDO

Authors Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl

Publication date 31 July 2012

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-011-9237-y

zbMATH Keywords

sequent calculusCraig interpolationPresburger arithmetic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Structure of proofs (03F07) First-order arithmetic and fragments (03F30) Interpolation, preservation, definability (03C40)

Recommendations

• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Interpolating quantifier-free Presburger arithmetic
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Interpolant based decision procedure for quantifier-free Presburger arithmetic
• Tools and Algorithms for the Construction and Analysis of Systems

Cites work

• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating theorem prover
• Constraint Solving for Interpolation
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Interpolant Generation for UTVPI
• Interpolants for Linear Arithmetic in SMT
• Interpolating quantifier-free Presburger arithmetic
• Lazy Abstraction with Interpolants
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Polynomial Algorithms for Computing the Smith and Hermite Normal Forms of an Integer Matrix

Cited in

(11)

• Reasoning in the theory of heap: satisfiability and interpolation
• Preface: Special issue on interpolation
• Parallelizing SMT solving: lazy decomposition and conciliation
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• On recursion-free Horn clauses and Craig interpolation
• Complete instantiation-based interpolation
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Interpolating quantifier-free Presburger arithmetic
• Craig interpolation with clausal first-order tableaux
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Interpolant based decision procedure for quantifier-free Presburger arithmetic

Describes a project that uses

Uses Software

• FOCI
• CSIsat
• OpenSMT
• Princess

This page was built for publication: An interpolating sequent calculus for quantifier-free Presburger arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438556)