Labelled interpolation systems for hyper-resolution, clausal, and local proofs
From MaRDI portal
Publication:286731
DOI10.1007/s10817-016-9364-6zbMath1356.68199OpenAlexW2222719317WikidataQ59463436 ScholiaQ59463436MaRDI QIDQ286731
Georg Weissenbacher, Matthias Schlaipfer
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Resolution proof transformation for compression and interpolation
- 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
- SAT-Based Synthesis Methods for Safety Specs
- 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
- Interpolant Strength
- 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
- Interpolation and Symbol Elimination
- Compression of Propositional Resolution Proofs via Partial Regularization
- Theory and Applications of Satisfiability Testing
- 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
- Complete instantiation-based interpolation
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Labelled interpolation systems for hyper-resolution, clausal, and local proofs
