Ground Interpolation for Combined Theories

DOI10.1007/978-3-642-02959-2_16zbMath1250.68188OpenAlexW1551465820MaRDI 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

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)

Related Items (11)

Interpolation systems for ground proofs in automated deduction: a survey ⋮ Satisfiability Modulo Theories ⋮ Constraint solving for interpolation ⋮ Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions ⋮ SMT proof checking using a logical framework ⋮ Complete instantiation-based interpolation ⋮ Resolution proof transformation for compression and interpolation ⋮ On Interpolation in Decision Procedures ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic ⋮ On interpolation in automated theorem proving

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

This page was built for publication: Ground Interpolation for Combined Theories