scientific article; zbMATH DE number 3583767
From MaRDI portal
Publication:4152212
zbMATH Open0375.02004MaRDI QIDQ4152212FDOQ4152212
Authors: Robert A. Reckhow, Stephen Cook 
Publication date: 1974
Title of this publication is not available (Why is that?)
Enumerative combinatorics (05A99) Analysis of algorithms and problem complexity (68Q25) Classical propositional logic (03B05)
Cited In (51)
- Proving the infeasibility of Horn formulas through read-once resolution
- Logical omniscience as infeasibility
- Substitution and Propositional Proof Complexity
- Characterizing propositional proofs as noncommutative formulas
- Proof Complexity Meets Algebra
- A proper hierarchy of propositional sequent calculi
- On a generalization of extended resolution
- On the complexity of regular resolution and the Davis-Putnam procedure
- Practical extraction of evidence terms from common-knowledge reasoning
- A note on some computationally difficult set covering problems
- Frege systems for extensible modal logics
- On the complexity of choosing the branching literal in DPLL
- The complexity of Gentzen systems for propositional logic
- Towards NP-P via proof complexity and search
- Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals
- Short proofs of the Kneser-Lovász coloring principle
- Semantics and proof-theory of depth bounded Boolean logics
- The proof complexity of analytic and clausal tableaux
- The NP search problems of Frege and extended Frege proofs
- Resolution and binary decision diagrams cannot simulate each other polynomially
- Proof complexity of non-classical logics
- Non-circular proofs and proof realization in modal logic
- Propositional proofs in Frege and extended Frege systems (abstract)
- Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
- Title not available (Why is that?)
- Optimal proof systems imply complete sets for promise classes
- An answer to an open problem of Urquhart
- Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
- Resolution with counting: dag-like lower bounds and different moduli
- Short propositional refutations for dense random 3CNF formulas
- Some remarks on lengths of propositional proofs
- On linear rewriting systems for Boolean logic and some applications to proof theory
- Complexity of translations from resolution to sequent calculus
- Making knowledge explicit: how hard it is
- A simulation of natural deduction and Gentzen sequent calculus
- Controlled integration of the cut rule into connection tableau calculi
- Craig interpolation with clausal first-order tableaux
- On the relative merits of path dissolution and the method of analytic tableaux
- NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
- Satisfiability problems for propositional calculi
- Tautology testing with a generalized matrix reduction method
- Extended clause learning
- The complexity of finding read-once NAE-resolution refutations
- Davis-Putnam resolution versus unrestricted resolution
- Witnessing matrix identities and proof complexity
- Non-elementary speed-ups in proof length by different variants of classical analytic calculi
- Generalisation of proof simulation procedures for Frege systems by M. L. Bonet and S. R. Buss
- Resolution remains hard under equivalence
- The intractability of resolution
- Classical logic, argument and dialectic
- Enumerating Independent Linear Inferences
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4152212)
