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
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 ⋮ Unnamed Item ⋮ 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 ⋮ Discretely ordered modules as a first-order extension of the cutting planes proof system ⋮ The cost of a cycle is a square ⋮ A note on constructive interpolation for the multi-modal logic \(K_m\) ⋮ Short Proofs of the Kneser-Lovász Coloring Principle ⋮ Cumulative Space in Black-White Pebbling and Resolution ⋮ Proof search on bilateralist judgments over non-deterministic semantics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Extracting a DPLL Algorithm ⋮ A Parameterized Halting Problem ⋮ Circuit principles and weak pigeonhole variants ⋮ Hardness assumptions in the foundations of theoretical computer science ⋮ Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\) ⋮ The state of SAT ⋮ Propositional Proofs in Frege and Extended Frege Systems (Abstract) ⋮ Propositional proof systems, the consistency of first order theories and the complexity of computations ⋮ European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium '88), Padova, 1988 ⋮ Correspondence analysis and automated proof-searching for first degree entailment ⋮ Characterizing Propositional Proofs as Noncommutative Formulas ⋮ Space Complexity in Polynomial Calculus ⋮ A reduction of proof complexity to computational complexity for 𝐴𝐶⁰[𝑝 Frege systems] ⋮ On the Power of Substitution in the Calculus of Structures ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Logical Closure Properties of Propositional Proof Systems ⋮ What is an inference rule? ⋮ Polynomial size proofs of the propositional pigeonhole principle ⋮ Limitations of Restricted Branching in Clause Learning ⋮ From QBFs to \textsf{MALL} and back via focussing ⋮ Simulating strong practical proof systems with extended resolution ⋮ Further oracles separating conjectures about incompleteness in the finite domain ⋮ Automatic theorem proving. II ⋮ Towards a Unified Complexity Theory of Total Functions ⋮ A Tight Karp-Lipton Collapse Result in Bounded Arithmetic ⋮ Witnessing matrix identities and proof complexity ⋮ Sufficient conditions for cut elimination with complexity analysis ⋮ Minimum propositional proof length is NP-hard to linearly approximate ⋮ INCOMPLETENESS IN THE FINITE DOMAIN ⋮ Tautologies from Pseudo-Random Generators ⋮ Lower bounds for cutting planes proofs with small coefficients ⋮ Propositional proof systems based on maximum satisfiability ⋮ On the Proof Complexity of Cut-Free Bounded Deep Inference ⋮ 2010 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '10 ⋮ Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds ⋮ Parameterized Bounded-Depth Frege Is Not Optimal ⋮ Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Buss ⋮ Grammar specification in categorial logics and theorem proving ⋮ Extended resolution simulates binary decision diagrams ⋮ Towards Hilbert's 24th Problem: Combinatorial Proof Invariants ⋮ Partially definable forcing and bounded arithmetic ⋮ An Upper Bound on the Space Complexity of Random Formulae in Resolution ⋮ The complexity of the Hajós calculus for planar graphs ⋮ Limitations of restricted branching in clause learning ⋮ Characterising tree-like Frege proofs for QBF ⋮ Several notes on the power of Gomory-Chvátal cuts ⋮ Polynomial-size Frege and resolution proofs of \(st\)-connectivity and Hex tautologies ⋮ Simulation of Natural Deduction and Gentzen Sequent Calculus ⋮ Frege systems for extensible modal logics ⋮ A Framework for Space Complexity in Algebraic Proof Systems ⋮ 2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02 ⋮ An oracle separating conjectures about incompleteness in the finite domain ⋮ INFORMAL PROOF, FORMAL PROOF, FORMALISM ⋮ Nondeterministic Instance Complexity and Proof Systems with Advice ⋮ 2004 Annual Meeting of the Association for Symbolic Logic ⋮ On the correspondence between arithmetic theories and propositional proof systems – a survey ⋮ Satisfiability via Smooth Pictures ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ Q-Resolution with Generalized Axioms ⋮ Transition systems for model generators—A unifying approach ⋮ THE INFORMATIONAL CONTENT OF CANONICAL DISJOINT NP-PAIRS ⋮ Does Advice Help to Prove Propositional Tautologies? ⋮ Characterizing the Existence of Optimal Proof Systems and Complete Sets for Promise Classes ⋮ ON THE PROOF COMPLEXITY OF THE NISAN–WIGDERSON GENERATOR BASED ON A HARD NP ∩ coNP FUNCTION ⋮ Random resolution refutations ⋮ Total Space in Resolution ⋮ DEHN FUNCTION AND LENGTH OF PROOFS ⋮ Do there exist complete sets for promise classes? ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ The complexity of analytic tableaux ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ On the proof complexity of logics of bounded branching ⋮ Computing (and Life) Is All about Tradeoffs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Resolution over linear equations modulo two ⋮ A lower bound for the complexity of Craig's interpolants in sentential logic ⋮ Expansion-based QBF solving versus Q-resolution ⋮ How QBF expansion makes strategy extraction hard ⋮ Integrating induction and coinduction via closure operators and proof cycles ⋮ On non-Abelian homomorphic public-key cryptosystems ⋮ Witnessing functions in bounded arithmetic and search problems ⋮ On Exponential Lower Bounds for Partially Ordered Resolution ⋮ Quasipolynomial size proofs of the propositional pigeonhole principle ⋮ Proof complexity of monotone branching programs ⋮ Synthetic tableaux: Minimal tableau search heuristics ⋮ The deduction rule and linear and near-linear proof simulations ⋮ Substitution and Propositional Proof Complexity ⋮ Hardness and optimality in QBF proof systems modulo NP ⋮ Proof complexity of symbolic QBF reasoning ⋮ 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 ⋮ The symmetry rule in propositional logic ⋮ The NP-hardness of finding a directed acyclic graph for regular resolution ⋮ Reduction of Hilbert-type proof systems to the if-then-else equational logic ⋮ Tuples of disjoint \(\mathsf{NP}\)-sets ⋮ Propositional consistency proofs ⋮ On meta complexity of propositional formulas and propositional proofs ⋮ Unrestricted resolution versus N-resolution ⋮ Meta-resolution: An algorithmic formalisation ⋮ Tractability of cut-free Gentzen type propositional calculus with permutation inference ⋮ Number of models and satisfiability of sets of clauses ⋮ Exponential lower bounds for the tree-like Hajós calculus ⋮ Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs ⋮ Interpolants, cut elimination and flow graphs for the propositional calculus ⋮ Towards a unified complexity theory of total functions ⋮ Lower bound techniques for QBF expansion ⋮ Resolution over linear equations and multilinear proofs ⋮ On semantic cutting planes with very small coefficients ⋮ Functional interpretations of feasibly constructive arithmetic ⋮ The relative complexity of analytic tableaux and SL-resolution ⋮ Exponential lower bounds for the pigeonhole principle ⋮ Cut formulas in propositional logic ⋮ On optimal heuristic randomized semidecision procedures, with applications to proof complexity and cryptography ⋮ Inseparability and strong hypotheses for disjoint NP pairs ⋮ On the power of clause-learning SAT solvers as resolution engines ⋮ Total nondeterministic Turing machines and a p-optimal proof system for SAT ⋮ Proof systems that take advice ⋮ The treewidth of proofs ⋮ Extension without cut ⋮ The deduction theorem for strong propositional proof systems ⋮ A direct construction of polynomial-size OBDD proof of pigeon hole problem ⋮ On the complexity of cutting-plane proofs ⋮ Understanding cutting planes for QBFs ⋮ Resolution with counting: dag-like lower bounds and different moduli ⋮ Building strategies into QBF proofs ⋮ Proof complexity of substructural logics ⋮ Quantum deduction rules ⋮ Hilbert-style axiomatization of first-degree entailment and a family of its extensions ⋮ Short propositional refutations for dense random 3CNF formulas ⋮ The complexity of Gentzen systems for propositional logic ⋮ A note on the computational complexity of the pure classical implication calculus ⋮ Finding a tree structure in a resolution proof is NP-complete ⋮ Substitution Frege and extended Frege proof systems in non-classical logics ⋮ Audiences in argumentation frameworks ⋮ Argumentation in artificial intelligence ⋮ Computational properties of argument systems satisfying graph-theoretic constraints ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ A new methodology for developing deduction methods ⋮ The proof complexity of analytic and clausal tableaux ⋮ Relative efficiency of propositional proof systems: Resolution vs. cut-free LK ⋮ Investigations on autark assignments ⋮ On an optimal propositional proof system and the structure of easy subsets of TAUT. ⋮ Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence ⋮ The intractability of resolution ⋮ Two party immediate response disputes: Properties and efficiency
This page was built for publication: The relative efficiency of propositional proof systems
