Labelled interpolation systems for hyper-resolution, clausal, and local proofs
From MaRDI portal
(Redirected from Publication:286731)
Recommendations
Cites work
- scientific article; zbMATH DE number 5510691 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 3254919 (Why is no real title available?)
- scientific article; zbMATH DE number 2243370 (Why is no real title available?)
- scientific article; zbMATH DE number 3199779 (Why is no real title available?)
- An interpolating theorem prover
- Automated Deduction – CADE-20
- Complete instantiation-based interpolation
- Compression of propositional resolution proofs via partial regularization
- Computer Aided Verification
- Constraint Solving for Interpolation
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Efficient Generation of Small Interpolants in CNF
- Efficient generation of Craig interpolants in satisfiability modulo theories
- Error invariants
- Generalised interpolation by solving recursion-free Horn clauses
- Ground Interpolation for the Theory of Equality
- Interpolant strength
- Interpolant strength revisited
- Interpolation and SAT-based model checking.
- Interpolation and Symbol Elimination
- Interpolation in Local Theory Extensions
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Lower bounds for resolution and cutting plane proofs and monotone computations
- On interpolation in decision procedures
- PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
- Playing in the grey area of proofs
- Propositional Interpolation and Abstract Interpretation
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Resolution With Merging
- Resolution proof transformation for compression and interpolation
- SAT-Based Model Checking without Unrolling
- SAT-Based Synthesis Methods for Safety Specs
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Tools and Algorithms for the Construction and Analysis of Systems
Cited in
(4)
This page was built for publication: Labelled interpolation systems for hyper-resolution, clausal, and local proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286731)
