Ground Interpolation for Combined Theories

DOI10.1007/978-3-642-02959-2_16zbMath1250.68188MaRDI QIDQ5191102

Cesare Tinelli, Sava Krstić, Amit Goel

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_16

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

03B35: Mechanization of proofs and logical operations

03C40: Interpolation, preservation, definability

Related Items

Quantifier-free interpolation in combinations of equality interpolating theories, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, Constraint solving for interpolation, SMT proof checking using a logical framework, On Interpolation in Decision Procedures

Uses Software

• CSIsat
• FOCI

Cites Work

• Unnamed Item
• Efficient theory combination via Boolean search
• An interpolating theorem prover
• Model-based Theory Combination
• Abstractions from proofs
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Ground Interpolation for the Theory of Equality
• Automated Deduction – CADE-20
• Constraint Solving for Interpolation
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Resolution With Merging
• Logic for Programming, Artificial Intelligence, and Reasoning
• Computer Aided Verification
• Lazy Abstraction with Interpolants
• Computer Aided Verification