Resolution proof transformation for compression and interpolation (Q479815): Difference between revisions

@@ Property / arXiv ID @@
+.2028
@@ Property / arXiv ID: 1307.2028 / rank @@
+Normal rank
@@ Property / cites work @@
+Solvable cases of the decision problem
@@ Property / cites work: Solvable cases of the decision problem / rank @@
+Normal rank
@@ Property / cites work @@
+Compressing Propositional Refutations
@@ Property / cites work: Compressing Propositional Refutations / rank @@
+Normal rank
@@ Property / cites work @@
+Data compression for proof replay
@@ Property / cites work: Data compression for proof replay / rank @@
+Normal rank
@@ Property / cites work @@
+Q4417909
@@ Property / cites work: Q4417909 / rank @@
+Normal rank
@@ Property / cites work @@
+Splitting on Demand in SAT Modulo Theories
@@ Property / cites work: Splitting on Demand in SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Compression of Propositional Resolution Proofs by Lowering Subproofs
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+SAT-Based Model Checking without Unrolling
@@ Property / cites work: SAT-Based Model Checking without Unrolling / rank @@
+Normal rank
@@ Property / cites work @@
+Q3181652
@@ Property / cites work: Q3181652 / rank @@
+Normal rank
@@ Property / cites work @@
+Approximating minimal unsatisfiable subformulae by means of adaptive core search
+Normal rank
@@ Property / cites work @@
+Resolution proof transformation for compression and interpolation
+Normal rank
@@ Property / cites work @@
+Proof Tree Preserving Interpolation
@@ Property / cites work: Proof Tree Preserving Interpolation / rank @@
+Normal rank
@@ Property / cites work @@
+A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
+Normal rank
@@ Property / cites work @@
+Efficient Interpolant Generation in Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Two Techniques for Minimizing Resolution Proofs
@@ Property / cites work: Two Techniques for Minimizing Resolution Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
+Normal rank
@@ Property / cites work @@
+A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
+Normal rank
@@ Property / cites work @@
+Interpolant Strength
@@ Property / cites work: Interpolant Strength / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Compression of Propositional Resolution Proofs via Partial Regularization
+Normal rank
@@ Property / cites work @@
+Untersuchungen über das logische Schliessen. I
@@ Property / cites work: Untersuchungen über das logische Schliessen. I / rank @@
+Normal rank
@@ Property / cites work @@
+Ground Interpolation for Combined Theories
@@ Property / cites work: Ground Interpolation for Combined Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q3506045
@@ Property / cites work: Q3506045 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3184604
@@ Property / cites work: Q3184604 / rank @@
+Normal rank
@@ Property / cites work @@
+Local-search extraction of mUSes
@@ Property / cites work: Local-search extraction of mUSes / rank @@
+Normal rank
@@ Property / cites work @@
+Proof-guided underapproximation-widening for multi-process systems
+Normal rank
@@ Property / cites work @@
+Improved Single Pass Algorithms for Resolution Proof Reduction
+Normal rank
@@ Property / cites work @@
+Abstractions from proofs
@@ Property / cites work: Abstractions from proofs / rank @@
+Normal rank
@@ Property / cites work @@
+DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Lower bounds for resolution and cutting plane proofs and monotone computations
+Normal rank
@@ Property / cites work @@
+An Efficient and Flexible Approach to Resolution Proof Reduction
+Normal rank
@@ Property / cites work @@
+Efficiently checking propositional refutations in HOL theorem provers
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank