Ground Interpolation for the Theory of Equality

DOI10.1007/978-3-642-00768-2_34zbMath1234.68257arXiv1111.5652OpenAlexW1528301227MaRDI QIDQ3617772

Amit Goel, Jim Grundy, Sava Krstić, Alexander Fuchs, Cesare Tinelli

Publication date: 31 March 2009

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1111.5652

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)

Related Items (11)

Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints ⋮ Satisfiability Modulo Theories ⋮ Complete instantiation-based interpolation ⋮ On Interpolation in Decision Procedures ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Interpolant Generation for UTVPI ⋮ Ground Interpolation for Combined Theories ⋮ Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic ⋮ Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Uses Software

• SMT-LIB
• FOCI
• DPT

Cites Work

• Model-theoretic methods in combined constraint satisfiability
• Cooperation of background reasoners in theory reasoning by residue sharing
• An interpolating theorem prover
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Automated Deduction – CADE-20
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Term Rewriting and Applications
• Computer Aided Verification

This page was built for publication: Ground Interpolation for the Theory of Equality