Ground interpolation for the theory of equality

DOI10.2168/LMCS-8(1:6)2012zbMATH Open1239.03022OpenAlexW1972614792MaRDI QIDQ2881073FDOQ2881073

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

Publication date: 3 April 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2168/lmcs-8(1:6)2012

Recommendations

• Ground Interpolation for the Theory of Equality
• Interpolation in local theory extensions
• Ground Interpolation for Combined Theories
• On interpolation in automated theorem proving
• Interpolants and Symbolic Model Checking

zbMATH Keywords

satisfiability modulo theorieslogical interpolation

Mathematics Subject Classification ID

Logic in computer science (03B70) Interpolation, preservation, definability (03C40)

Cited In (5)

• Interpolation systems for ground proofs in automated deduction: a survey
• Parallelizing SMT solving: lazy decomposition and conciliation
• On interpolation in automated theorem proving
• Ground-theoretic equivalence
• Ground Interpolation for the Theory of Equality

Uses Software

• SMT-LIB
• SIMPLIFY
• FOCI
• DPT

This page was built for publication: Ground interpolation for the theory of equality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881073)