scientific article; zbMATH DE number 3583767

Cited in

(51)

Logical omniscience as infeasibility
Enumerating Independent Linear Inferences
Characterizing propositional proofs as noncommutative formulas
Proof Complexity Meets Algebra
Substitution and Propositional Proof Complexity
A proper hierarchy of propositional sequent calculi
Proving the infeasibility of Horn formulas through read-once resolution
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
Frege systems for extensible modal logics
On the complexity of choosing the branching literal in DPLL
A note on some computationally difficult set covering problems
Towards NP-P via proof complexity and search
The complexity of Gentzen systems for propositional logic
Short proofs of the Kneser-Lovász coloring principle
Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals
Semantics and proof-theory of depth bounded Boolean logics
The proof complexity of analytic and clausal tableaux
Resolution and binary decision diagrams cannot simulate each other polynomially
The NP search problems of Frege and extended Frege proofs
Non-circular proofs and proof realization in modal logic
Proof complexity of non-classical logics
Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
Optimal proof systems imply complete sets for promise classes
Propositional proofs in Frege and extended Frege systems (abstract)
An answer to an open problem of Urquhart
scientific article; zbMATH DE number 7350778 (Why is no real title available?)
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
Making knowledge explicit: how hard it is
Complexity of translations from resolution to sequent calculus
Controlled integration of the cut rule into connection tableau calculi
A simulation of natural deduction and Gentzen sequent calculus
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
Tautology testing with a generalized matrix reduction method
Extended clause learning
Satisfiability problems for propositional calculi
Davis-Putnam resolution versus unrestricted resolution
The complexity of finding read-once NAE-resolution refutations
Witnessing matrix identities and proof complexity
Non-elementary speed-ups in proof length by different variants of classical analytic calculi
Resolution remains hard under equivalence
Generalisation of proof simulation procedures for Frege systems by M. L. Bonet and S. R. Buss
The intractability of resolution
Classical logic, argument and dialectic

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)