Recommendations
Cites work
- Abstractions from proofs
- An interpolating theorem prover
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Automated Deduction – CADE-20
- Computer Aided Verification
- Constraint Solving for Interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Efficient theory combination via Boolean search
- Ground Interpolation for the Theory of Equality
- scientific article; zbMATH DE number 1470716 (Why is no real title available?)
- Interpolation and SAT-based model checking.
- Lazy Abstraction with Interpolants
- Logic for Programming, Artificial Intelligence, and Reasoning
- Model-based theory combination
- Resolution With Merging
Cited in
(17)- On interpolation in automated theorem proving
- SMT proof checking using a logical framework
- Interpolation systems for ground proofs in automated deduction: a survey
- Ground interpolation for the theory of equality
- Efficient generation of Craig interpolants in satisfiability modulo theories
- On interpolation in decision procedures
- Satisfiability modulo theories
- Interpolation in Local Theory Extensions
- Ground Interpolation for the Theory of Equality
- Resolution proof transformation for compression and interpolation
- Proof tree preserving interpolation
- Automated Deduction – CADE-20
- Quantifier-free interpolation in combinations of equality interpolating theories
- Complete instantiation-based interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Constraint solving for interpolation
- Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions
This page was built for publication: Ground Interpolation for Combined Theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5191102)
