An interpolating sequent calculus for quantifier-free Presburger arithmetic

DOI10.1007/978-3-642-14203-1_33MaRDI QIDQ5747778zbMATH OpenOpenAlexFDO

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

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

Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40) First-order arithmetic and fragments (03F30)

Recommendations

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

Cites work

• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• An interpolating theorem prover
• Constraint Solving for Interpolation
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3199779 (Why is no real title available?)
• Interpolant Generation for UTVPI
• Interpolants for Linear Arithmetic in SMT
• 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

(17)

• The map equality domain
• An interpolating theorem prover
• 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
• 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
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An extension of lazy abstraction with interpolation for programs with arrays
• Interpolating quantifier-free Presburger arithmetic
• Quantifier-free interpolation in combinations of equality interpolating theories
• Interpolant based decision procedure for quantifier-free Presburger arithmetic
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

Describes a project that uses

Uses Software

• 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 Q5747778)