scientific article; zbMATH DE number 3583767

Cited in

(55)

The intractability of resolution
An answer to an open problem of Urquhart
Tautology testing with a generalized matrix reduction method
On the complexity of regular resolution and the Davis-Putnam procedure
The complexity of Gentzen systems for propositional logic
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
Davis-Putnam resolution versus unrestricted resolution
Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
Optimal proof systems imply complete sets for promise classes
Resolution and binary decision diagrams cannot simulate each other polynomially
The proof complexity of analytic and clausal tableaux
Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
Short proofs of the Kneser-Lovász coloring principle
Classical logic, argument and dialectic
Some remarks on lengths of propositional proofs
Resolution remains hard under equivalence
On a generalization of extended resolution
On the complexity of choosing the branching literal in DPLL
Resolution with counting: dag-like lower bounds and different moduli
Non-circular proofs and proof realization in modal logic
Making knowledge explicit: how hard it is
Frege systems for extensible modal logics
Craig interpolation with clausal first-order tableaux
On linear rewriting systems for Boolean logic and some applications to proof theory
Propositional proofs in Frege and extended Frege systems (abstract)
NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
Semantics and proof-theory of depth bounded Boolean logics
Satisfiability problems for propositional calculi
A note on some computationally difficult set covering problems
Logical omniscience as infeasibility
Towards NP-P via proof complexity and search
Characterizing propositional proofs as noncommutative formulas
Non-elementary speed-ups in proof length by different variants of classical analytic calculi
Proof Complexity Meets Algebra
Witnessing matrix identities and proof complexity
Generalisation of proof simulation procedures for Frege systems by M. L. Bonet and S. R. Buss
A simulation of natural deduction and Gentzen sequent calculus
DRAT and propagation redundancy proofs without new variables
Substitution and Propositional Proof Complexity
Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals
The complexity of finding read-once NAE-resolution refutations
Complexity of translations from resolution to sequent calculus
The NP search problems of Frege and extended Frege proofs
Practical extraction of evidence terms from common-knowledge reasoning
Proof complexity of non-classical logics
Enumerating Independent Linear Inferences
Extended clause learning
Proving the infeasibility of Horn formulas through read-once resolution
Numeral completeness of weak theories of arithmetic
Feasibly constructive proofs and the propositional calculus (preliminary version)
The relative efficiency of propositional proof systems
A classical proof system for quantum unsatisfiability, based on a matrix Nullstellensatz
Short propositional refutations for dense random 3CNF formulas

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)