scientific article; zbMATH DE number 3583767

zbMath0375.02004MaRDI QIDQ4152212

Robert A. Reckhow, Stephen A. Cook

Publication date: 1974

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Enumerative combinatorics (05A99) Classical propositional logic (03B05)

Related Items

The NP Search Problems of Frege and Extended Frege Proofs, On the relative merits of path dissolution and the method of analytic tableaux, Controlled integration of the cut rule into connection tableau calculi, A proper hierarchy of propositional sequent calculi, Short proofs of the Kneser-Lovász coloring principle, Davis-Putnam resolution versus unrestricted resolution, Some remarks on lengths of propositional proofs, Propositional Proofs in Frege and Extended Frege Systems (Abstract), Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Characterizing Propositional Proofs as Noncommutative Formulas, Craig interpolation with clausal first-order tableaux, An answer to an open problem of Urquhart, Semantics and proof-theory of depth bounded Boolean logics, Tautology testing with a generalized matrix reduction method, Logical omniscience as infeasibility, Unnamed Item, Extended clause learning, Optimal proof systems imply complete sets for promise classes, Towards NP-P via proof complexity and search, Enumerating Independent Linear Inferences, Resolution and binary decision diagrams cannot simulate each other polynomially, Non-elementary speed-ups in proof length by different variants of classical analytic calculi, On linear rewriting systems for Boolean logic and some applications to proof theory, Classical logic, argument and dialectic, Proof Complexity Meets Algebra, Resolution remains hard under equivalence, On a generalization of extended resolution, Witnessing matrix identities and proof complexity, On the complexity of choosing the branching literal in DPLL, Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Buss, Practical extraction of evidence terms from common-knowledge reasoning, Making knowledge explicit: how hard it is, Satisfiability problems for propositional calculi, Simulation of Natural Deduction and Gentzen Sequent Calculus, Frege systems for extensible modal logics, A note on some computationally difficult set covering problems, Resolution with counting: dag-like lower bounds and different moduli, On the complexity of regular resolution and the Davis-Putnam procedure, Short propositional refutations for dense random 3CNF formulas, Proof Complexity of Non-classical Logics, The complexity of Gentzen systems for propositional logic, NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability, The Complexity of Finding Read-Once NAE-Resolution Refutations, Complexity of translations from resolution to sequent calculus, The proof complexity of analytic and clausal tableaux, Relative efficiency of propositional proof systems: Resolution vs. cut-free LK, Non-circular proofs and proof realization in modal logic, The intractability of resolution, Substitution and Propositional Proof Complexity, Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals