Relative efficiency of propositional proof systems: Resolution vs. cut-free LK

DOI10.1016/S0168-0072(00)00005-1zbMath0959.03045OpenAlexW2062949469MaRDI QIDQ1577476

Noriko H. Arai

Publication date: 4 September 2000

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(00)00005-1

zbMATH Keywords

resolutioncut-eliminationproof complexitydirected acyclic graphspropositional proof systemcut-free LK

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Classical propositional logic (03B05) Complexity of proofs (03F20)

Related Items

Reduction of Hilbert-type proof systems to the if-then-else equational logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tractability of cut-free Gentzen type propositional calculus with permutation inference
• Cut formulas in propositional logic
• Short proofs for tricky formulas
• Gentzen-type systems, resolution and tableaux
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• A proper hierarchy of propositional sequent calculi
• The relative complexity of resolution and cut-free Gentzen systems
• No feasible monotone interpolation for simple combinatorial reasoning
• Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II
• The symmetry rule in propositional logic
• Short proofs are narrow—resolution made simple
• Regular Resolution Versus Unrestricted Resolution
• The relative efficiency of propositional proof systems
• Bounds for proof-search and speed-up in the predicate calculus
• Lower bounds to the size of constant-depth propositional proofs
• A Computing Procedure for Quantification Theory

This page was built for publication: Relative efficiency of propositional proof systems: Resolution vs. cut-free LK