The relative efficiency of propositional proof systems

Cited in

(only showing first 100 items - show all)

Quantum deduction rules
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
A new methodology for developing deduction methods
The intractability of resolution
Resolution vs. cutting plane solution of inference problems: Some computational experience
Seventy-five problems for testing automatic theorem provers
Propositional consistency proofs
Unrestricted resolution versus N-resolution
The complexity of Gentzen systems for propositional logic
A note on the computational complexity of the pure classical implication calculus
On the modelling of search in theorem proving -- towards a theory of strategy analysis
Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
A kind of logical compilation for knowledge bases
A lower bound for tree 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
Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
\(\text{Count}(q)\) does not imply \(\text{Count}(p)\)
Some consequences of cryptographical conjectures for \(S_2^1\) and EF
Optimal proof systems imply complete sets for promise classes
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
Homomorphisms of conjunctive normal forms.
Reduction of Hilbert-type proof systems to the if-then-else equational logic
The proof complexity of analytic and clausal tableaux
Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
On space and depth in resolution
Short proofs of the Kneser-Lovász coloring principle
A note about k-DNF resolution
A semantic framework for proof evidence
Cliques enumeration and tree-like resolution proofs
Towards a unified complexity theory of total functions
On semantic cutting planes with very small coefficients
Understanding cutting planes for QBFs
Investigations on autark assignments
On an optimal propositional proof system and the structure of easy subsets of TAUT.
Monotone simulations of non-monotone proofs.
On the automatizability of resolution and related propositional proof systems
On the complexity of resolution with bounded conjunctions
Some remarks on lengths of propositional proofs
Cutting planes, connectivity, and threshold logic
An exponential separation between the parity principle and the pigeonhole principle
Short resolution proofs for a sequence of tricky formulas
Proof system representations of degrees of disjoint NP-pairs
On a generalization of extended resolution
The symmetry rule in propositional logic
Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs
Lower bound techniques for QBF expansion
Total nondeterministic Turing machines and a p-optimal proof system for SAT
The treewidth of proofs
Resolution with counting: dag-like lower bounds and different moduli
Building strategies into QBF proofs
Proof complexity of substructural logics
Hilbert-style axiomatization of first-degree entailment and a family of its extensions
Bounded-depth Frege complexity of Tseitin formulas for all graphs
On the proof complexity of logics of bounded branching
How QBF expansion makes strategy extraction hard
Integrating induction and coinduction via closure operators and proof cycles
Proof complexity of monotone branching programs
Synthetic tableaux: Minimal tableau search heuristics
Hardness and optimality in QBF proof systems modulo NP
Proof complexity of symbolic QBF reasoning
A note on constructive interpolation for the multi-modal logic \(K_m\)
Proof search on bilateralist judgments over non-deterministic semantics
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
Propositional proof systems based on maximum satisfiability
Partially definable forcing and bounded arithmetic
The complexity of the Hajós calculus for planar graphs
Limitations of restricted branching in clause learning
Characterising tree-like Frege proofs for QBF
An oracle separating conjectures about incompleteness in the finite domain
Random resolution refutations
Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
Resolution over linear equations modulo two
Expansion-based QBF solving versus Q-resolution
Quasipolynomial size proofs of the propositional pigeonhole principle
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}}\)
Sufficient conditions for cut elimination with complexity analysis
Extended resolution simulates binary decision diagrams
Several notes on the power of Gomory-Chvátal cuts
Polynomial-size Frege and resolution proofs of \(st\)-connectivity and Hex tautologies
Frege systems for extensible modal logics
On non-Abelian homomorphic public-key cryptosystems
The state of SAT
Correspondence analysis and automated proof-searching for first degree entailment
Minimum propositional proof length is NP-hard to linearly approximate
Tautologies from pseudo-random generators
A framework for space complexity in algebraic proof systems
Informal proof, formal proof, formalism

This page was built for publication: The relative efficiency of propositional proof systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4194955)