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_8zbMATH Open1348.68123OpenAlexW194239260MaRDI QIDQ3172885FDOQ3172885
Authors: Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise 
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
Recommendations
Data structures (68P05) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Simplification by Cooperating Decision Procedures
- Title not available (Why is that?)
- Term Rewriting and All That
- 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
- Automated Deduction – CADE-20
- Constraint Solving for Interpolation
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Negative-cycle detection algorithms
- Rewriting-based quantifier-free interpolation for a theory of arrays
Cited In (6)
- Interpolation systems for ground proofs in automated deduction: a survey
- Efficient interpolation for the theory of arrays
- Rewriting-based quantifier-free interpolation for a theory of arrays
- Quantifier-free interpolation in combinations of equality interpolating theories
- Solving and interpolating constant arrays based on weak equivalences
- Quantifier-free interpolation of a theory of arrays
Uses Software
This page was built for publication: A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172885)
