Quantifier-free interpolation in combinations of equality interpolating theories
From MaRDI portal
Publication:5410332
DOI10.1145/2490253zbMath1287.03068MaRDI QIDQ5410332
Silvio Ranise, Silvio Ghilardi, Roberto Bruttomesso
Publication date: 16 April 2014
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2490253
satisfiability modulo theories; Craig interpolation theorem; combined interpolation; strong amalgamability
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
03C40: Interpolation, preservation, definability
Related Items
Unnamed Item, Interpolation Results for Arrays with Length and MaxDiff, Interpolation systems for ground proofs in automated deduction: a survey, Parallelizing SMT solving: lazy decomposition and conciliation, Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes), Combination of uniform interpolants via Beth definability, Combined covers and Beth definability, Interpolation and amalgamation for arrays with MaxDiff, Model completeness, covers and superposition, On invariant synthesis for parametric systems, On interpolation in automated theorem proving, Modularity results for interpolation, amalgamation and superamalgamation, On Interpolation and Symbol Elimination in Theory Extensions
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model-theoretic methods in combined constraint satisfiability
- Constraint solving for interpolation
- Amalgamation properties and interpolation theorems for equational theories
- Fourier-Motzkin elimination and its dual
- The intersection property of amalgamations
- An interpolating theorem prover
- Quantifier-Free Interpolation of a Theory of Arrays
- Lazy Abstraction with Interpolants for Arrays
- 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
- Universal relational systems
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Abstractions from proofs
- Interpolation in Local Theory Extensions
- Ground Interpolation for the Theory of Equality
- Simplification by Cooperating Decision Procedures
- Reasoning About Recursively Defined Data Structures
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Tools and Algorithms for the Construction and Analysis of Systems
- Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
- Automated Deduction – CADE-20
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Applications and Theory of Petri Nets 2005
- Computer Aided Verification
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Tools and Algorithms for the Construction and Analysis of Systems
