Labelled interpolation systems for hyper-resolution, clausal, and local proofs
From MaRDI portal
Publication:286731
DOI10.1007/S10817-016-9364-6zbMATH Open1356.68199OpenAlexW2222719317WikidataQ59463436 ScholiaQ59463436MaRDI QIDQ286731FDOQ286731
Authors: Matthias Schlaipfer, Georg Weissenbacher 
Publication date: 25 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-016-9364-6
Recommendations
Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)
Cites Work
- Theory and Applications of Satisfiability Testing
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interpolant strength
- Resolution proof transformation for compression and interpolation
- Title not available (Why is that?)
- Interpolation and SAT-based model checking.
- SAT-Based Synthesis Methods for Safety Specs
- Title not available (Why is that?)
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- An interpolating theorem prover
- Interpolant strength revisited
- Efficient Generation of Small Interpolants in CNF
- PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
- Playing in the grey area of proofs
- Efficient generation of Craig interpolants in satisfiability modulo theories
- On interpolation in decision procedures
- SAT-Based Model Checking without Unrolling
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Propositional Interpolation and Abstract Interpretation
- Interpolation in Local Theory Extensions
- Ground Interpolation for the Theory of Equality
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Error invariants
- Generalised interpolation by solving recursion-free Horn clauses
- Interpolation and Symbol Elimination
- Compression of propositional resolution proofs via partial regularization
- Automated Deduction – CADE-20
- Constraint Solving for Interpolation
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Resolution With Merging
- Theory and Applications of Satisfiability Testing
- Computer Aided Verification
- Title not available (Why is that?)
- Complete instantiation-based interpolation
- Tools and Algorithms for the Construction and Analysis of Systems
Cited In (4)
Uses Software
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)
