A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints

DOI10.1007/978-3-642-24364-6_8zbMath1348.68123OpenAlexW194239260MaRDI QIDQ3172885

Silvio Ghilardi, Silvio Ranise, Roberto Bruttomesso

Publication date: 7 October 2011

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24364-6_8

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Data structures (68P05)

Related Items (2)

Interpolation systems for ground proofs in automated deduction: a survey ⋮ Quantifier-free interpolation in combinations of equality interpolating theories

Uses Software

• Princess
• OpenSMT
• FOCI

Cites Work

• An interpolating theorem prover
• Efficient generation of craig interpolants in satisfiability modulo theories
• Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
• Abstractions from proofs
• Ground Interpolation for the Theory of Equality
• Simplification by Cooperating Decision Procedures
• Negative-cycle detection algorithms
• Term Rewriting and All That
• Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
• Automated Deduction – CADE-20
• Constraint Solving for Interpolation
• An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
• Unnamed Item

This page was built for publication: A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints