The relative efficiency of propositional proof systems
From MaRDI portal
Publication:4194955
DOI10.2307/2273702zbMath0408.03044OpenAlexW1988083342MaRDI QIDQ4194955
Robert A. Reckhow, Stephen A. Cook
Publication date: 1979
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2273702
Complexity of ProofsExtended Frege SystemsNatural Deduction SystemsPropositional Proof SystemPropositional Tautology
Related Items (only showing first 100 items - show all)
Narrow Proofs May Be Maximally Long ⋮ The NP Search Problems of Frege and Extended Frege Proofs ⋮ PROOF COMPLEXITIES ON A CLASS OF BALANCED FORMULAS IN SOME PROPOSITIONAL SYSTEMS ⋮ Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ On an optimal quantified propositional proof system nal proof system and a complete language for NP ∩ co-NP for NP ∩ co-NP ⋮ An Analytic Propositional Proof System on Graphs ⋮ Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds ⋮ Implicit proofs ⋮ INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH ⋮ Unnamed Item ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ NEW RELATIONS AND SEPARATIONS OF CONJECTURES ABOUT INCOMPLETENESS IN THE FINITE DOMAIN ⋮ ON NON-MONOTONOUS PROPERTIES OF SOME CLASSICAL AND NONCLASSICAL PROPOSITIONAL PROOF SYSTEMS ⋮ The power of the binary value principle ⋮ Combinatorial flows as bicolored atomic flows ⋮ Circular (Yet Sound) Proofs in Propositional Logic ⋮ Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas ⋮ A remark on pseudo proof systems and hard instances of the satisfiability problem ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Enumerating Independent Linear Inferences ⋮ A System of Interaction and Structure III: The Complexity of BV and Pomset Logic ⋮ Towards Uniform Certification in QBF ⋮ Non-transitive correspondence analysis ⋮ Space characterizations of complexity measures and size-space trade-offs in propositional proof systems ⋮ INTERLEAVING LOGIC AND COUNTING ⋮ ON THE EXISTENCE OF STRONG PROOF COMPLEXITY GENERATORS ⋮ An Introduction to Lower Bounds on Resolution Proof Systems ⋮ Unnamed Item ⋮ An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams ⋮ ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES ⋮ Classes of hard formulas for QBF resolution ⋮ Certified dominance and symmetry breaking for combinatorial optimisation ⋮ Unnamed Item ⋮ Should Decisions in QCDCL Follow Prefix Order? ⋮ Unnamed Item ⋮ The Complexity of Propositional Proofs ⋮ Reductions for non-clausal theorem proving ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ The Deduction Theorem for Strong Propositional Proof Systems ⋮ Parameterized Complexity of DPLL Search Procedures ⋮ The search efficiency of theorem proving strategies ⋮ Unnamed Item ⋮ Supercritical Space-Width Trade-offs for Resolution ⋮ Proof Complexity of Non-classical Logics ⋮ Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent ⋮ Propositional proof complexity ⋮ Unnamed Item ⋮ P-Optimal Proof Systems for Each NP-Set but no Complete Disjoint NP-Pairs Relative to an Oracle ⋮ Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs ⋮ Unnamed Item ⋮ Frege proof system and TNC° ⋮ Unnamed Item ⋮ Reflections on Proof Complexity and Counting Principles ⋮ MaxSAT Resolution and Subcube Sums ⋮ Monotone simulations of non-monotone proofs. ⋮ On space and depth in resolution ⋮ A kind of logical compilation for knowledge bases ⋮ On the automatizability of resolution and related propositional proof systems ⋮ A lower bound for tree resolution ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Proof complexity of modal resolution ⋮ On the complexity of resolution with bounded conjunctions ⋮ Nondeterministic functions and the existence of optimal proof systems ⋮ Substitutions into propositional tautologies ⋮ Short proofs of the Kneser-Lovász coloring principle ⋮ A note about \(k\)-DNF resolution ⋮ ALOGTIME and a conjecture of S. A. Cook ⋮ The relative complexity of resolution and cut-free Gentzen systems ⋮ Davis-Putnam resolution versus unrestricted resolution ⋮ Resolution vs. cutting plane solution of inference problems: Some computational experience ⋮ Seventy-five problems for testing automatic theorem provers ⋮ Some remarks on lengths of propositional proofs ⋮ Cutting planes, connectivity, and threshold logic ⋮ Canonical disjoint NP-pairs of propositional proof systems ⋮ Proof complexity in algebraic systems and bounded depth Frege systems with modular counting ⋮ \(\text{Count}(q)\) does not imply \(\text{Count}(p)\) ⋮ An exponential separation between the parity principle and the pigeonhole principle ⋮ Some consequences of cryptographical conjectures for \(S_2^1\) and EF ⋮ Short resolution proofs for a sequence of tricky formulas ⋮ Relativization makes contradictions harder for resolution ⋮ Classes of representable disjoint \textsf{NP}-pairs ⋮ Speedup for natural problems and noncomputability ⋮ Extended clause learning ⋮ Optimal proof systems imply complete sets for promise classes ⋮ Towards NP-P via proof complexity and search ⋮ Improved bounds on the weak pigeonhole principle and infinitely many primes from weaker axioms ⋮ On reducibility and symmetry of disjoint NP pairs. ⋮ Algebraic proof systems over formulas. ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ Proof system representations of degrees of disjoint NP-pairs ⋮ Homomorphisms of conjunctive normal forms. ⋮ A semantic framework for proof evidence ⋮ A note on SAT algorithms and proof complexity ⋮ On theories of bounded arithmetic for \(\mathrm{NC}^1\) ⋮ Cliques enumeration and tree-like resolution proofs ⋮ Algebraic proofs over noncommutative formulas ⋮ Parameterized proof complexity ⋮ Proof complexity of propositional default logic ⋮ Resolution proofs of generalized pigeonhole principles ⋮ On a generalization of extended resolution
This page was built for publication: The relative efficiency of propositional proof systems
