On Interpolation in Decision Procedures
From MaRDI portal
Publication:3010355
DOI10.1007/978-3-642-22119-4_1zbMath1331.68198OpenAlexW78903979MaRDI QIDQ3010355
Maria Paola Bonacina, Moa Johansson
Publication date: 1 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22119-4_1
Related Items
Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Craig interpolation with clausal first-order tableaux ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Craig interpolation in the presence of unreliable connectives ⋮ On interpolation in automated theorem proving
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- On deciding satisfiability by theorem proving with speculative inferences
- On the mechanical derivation of loop invariants
- An interpolating theorem prover
- Model-based Theory Combination
- Abstractions from proofs
- Solving SAT and SAT Modulo Theories
- Propositional Interpolation and Abstract Interpretation
- Ground Interpolation for the Theory of Equality
- Interpolant Strength
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Interpolant Generation for UTVPI
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Abstract canonical inference
- Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
- Automated Deduction – CADE-20
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Interpolation and Symbol Elimination in Vampire
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Computer Aided Verification
