Ground Interpolation for Combined Theories
From MaRDI portal
Publication:5191102
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
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)
Related Items
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
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