On interpolation in decision procedures

DOI10.1007/978-3-642-22119-4_1MaRDI QIDQ3010355zbMATH OpenOpenAlexFDO

Authors 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

Mathematics Subject Classification ID

Recommendations

• Interpolation systems for ground proofs in automated deduction: a survey
• Constraint Solving for Interpolation
• Constraint solving for interpolation
• Complete instantiation-based interpolation
• On interpolation in automated theorem proving

Cites work

• Abstract canonical inference
• Abstractions from proofs
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating theorem prover
• Automated Deduction – CADE-20
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Fast Decision Procedures Based on Congruence Closure
• Ground Interpolation for Combined Theories
• Ground Interpolation for the Theory of Equality
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• Interpolant Generation for UTVPI
• Interpolant strength
• Interpolation and SAT-based model checking.
• Interpolation and Symbol Elimination
• Interpolation and symbol elimination in Vampire
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lazy satisfiability modulo theories
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Model-based theory combination
• On deciding satisfiability by theorem proving with speculative inferences
• On the mechanical derivation of loop invariants
• Propositional Interpolation and Abstract Interpretation
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Rewriting-based quantifier-free interpolation for a theory of arrays
• Simplification by Cooperating Decision Procedures
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)

Cited in

(7)

• Craig interpolation in the presence of unreliable connectives
• On interpolation in automated theorem proving
• Craig interpolation with clausal first-order tableaux
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• Interpolation systems for ground proofs in automated deduction: a survey
• Point decisions for interval-identified parameters
• Quantifier-free interpolation in combinations of equality interpolating theories

Describes a project that uses

Uses Software

• Princess
• FOCI

This page was built for publication: On interpolation in decision procedures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3010355)