Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic

DOI10.1007/978-3-642-18275-4_8zbMath1318.03045arXiv1011.1036OpenAlexW3138202464MaRDI QIDQ3075472

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

Publication date: 15 February 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1011.1036

Mathematics Subject Classification ID

Logic in computer science (03B70) Interpolation, preservation, definability (03C40)

Related Items (11)

Interpolation systems for ground proofs in automated deduction: a survey ⋮ Not all bugs are created equal, but robust reachability can tell the difference ⋮ 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 ⋮ Complete instantiation-based interpolation ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations ⋮ Reasoning in the theory of heap: satisfiability and interpolation

Uses Software

• QPA
• SIMPLIFY
• Princess
• FOCI

Cites Work

• Unnamed Item
• An interpolating theorem prover
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Simplify: a theorem prover for program checking
• Ground Interpolation for the Theory of Equality
• Interpolant Strength
• Presburger arithmetic with unary predicates is Π₁¹ complete
• Automated Deduction – CADE-20
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
• Verification, Model Checking, and Abstract Interpretation
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic