Quantifier-free interpolation in combinations of equality interpolating theories

DOI10.1145/2490253zbMath1287.03068OpenAlexW2026276439MaRDI 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

zbMATH Keywords

satisfiability modulo theoriesCraig interpolation theoremcombined interpolationstrong amalgamability

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)

Related Items (13)

Interpolation systems for ground proofs in automated deduction: a survey ⋮ Modularity results for interpolation, amalgamation and superamalgamation ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Unnamed Item ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ On Interpolation and Symbol Elimination in Theory Extensions ⋮ Model completeness, covers and superposition ⋮ On invariant synthesis for parametric systems ⋮ Combination of uniform interpolants via Beth definability ⋮ Combined covers and Beth definability ⋮ On interpolation in automated theorem proving

Uses Software

• z3
• Princess
• CSIsat
• FOCI
• SAFARI

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

This page was built for publication: Quantifier-free interpolation in combinations of equality interpolating theories