The complexity of Gentzen systems for propositional logic

DOI10.1016/0304-3975(89)90147-3zbMath0688.03039OpenAlexW2009733922MaRDI QIDQ1263584

Alasdair Urquhart

Publication date: 1989

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90147-3

zbMATH Keywords

complexity of Gentzen-style systems for propositional logic

Mathematics Subject Classification ID

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

Related Items

A proper hierarchy of propositional sequent calculi, The relative complexity of resolution and cut-free Gentzen systems, Seventy-five problems for testing automatic theorem provers, An answer to an open problem of Urquhart, Reduction of Hilbert-type proof systems to the if-then-else equational logic, Tractability of cut-free Gentzen type propositional calculus with permutation inference, Simulation of Natural Deduction and Gentzen Sequent Calculus, A Measure of Logical Inference and Its Game Theoretical Applications, Argumentation in artificial intelligence, A Logical Autobiography, Two party immediate response disputes: Properties and efficiency

Cites Work

• A note on regular resolution
• A simplified proof that regular resolution is exponential
• On the complexity of regular resolution and the Davis-Putnam procedure
• The relative efficiency of propositional proof systems
• Bounds for proof-search and speed-up in the predicate calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item