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
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
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 (2)
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)
