Resolution proof transformation for compression and interpolation
From MaRDI portal
Publication:479815
DOI10.1007/s10703-014-0208-xzbMath1317.68123arXiv1307.2028OpenAlexW2032089673MaRDI QIDQ479815
Aliaksei Tsitovich, Natasha Sharygina, Roberto Bruttomesso, Simone Fulvio Rollini
Publication date: 5 December 2014
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1307.2028
Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40) Complexity of proofs (03F20)
Related Items
Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Proof tree preserving tree interpolation ⋮ Satisfiability Modulo Theories ⋮ Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic ⋮ Optimization techniques for Craig interpolant compaction in unbounded model checking ⋮ Resolution proof transformation for compression and interpolation ⋮ Exploiting partial variable assignment in interpolation-based model checking
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Resolution proof transformation for compression and interpolation
- Efficiently checking propositional refutations in HOL theorem provers
- Data compression for proof replay
- Approximating minimal unsatisfiable subformulae by means of adaptive core search
- Untersuchungen über das logische Schliessen. I
- Local-search extraction of mUSes
- Solvable cases of the decision problem
- Compression of Propositional Resolution Proofs by Lowering Subproofs
- SAT-Based Model Checking without Unrolling
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Abstractions from proofs
- A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
- Interpolant Strength
- 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
- Improved Single Pass Algorithms for Resolution Proof Reduction
- Two Techniques for Minimizing Resolution Proofs
- Compressing Propositional Refutations
- Ground Interpolation for Combined Theories
- Compression of Propositional Resolution Proofs via Partial Regularization
- Proof-guided underapproximation-widening for multi-process systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Science Logic
- Proof Tree Preserving Interpolation
- Splitting on Demand in SAT Modulo Theories
- An Efficient and Flexible Approach to Resolution Proof Reduction
- Automated Deduction – CADE-20
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Theory and Applications of Satisfiability Testing
- Computer Aided Verification
- Computer Aided Verification
- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
