The complexity of Gentzen systems for propositional logic

DOI10.1016/0304-3975(89)90147-3MaRDI QIDQ1263584zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 4114609
• scientific article; zbMATH DE number 1390276
• Complexity of deductions in a system of classical propositional calculus
• Gentzen-like systems for partial propositional calculi. I. II
• A note on the complexity of propositional Hoare logic
• The Complexity of Propositional Proofs
• The Complexity of Propositional Proofs
• scientific article; zbMATH DE number 1156870
• scientific article; zbMATH DE number 1860672

Cites work

• scientific article; zbMATH DE number 3904558 (Why is no real title available?)
• scientific article; zbMATH DE number 3458034 (Why is no real title available?)
• scientific article; zbMATH DE number 3482343 (Why is no real title available?)
• scientific article; zbMATH DE number 3557241 (Why is no real title available?)
• scientific article; zbMATH DE number 3583767 (Why is no real title available?)
• scientific article; zbMATH DE number 619541 (Why is no real title available?)
• scientific article; zbMATH DE number 3228218 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3420722 (Why is no real title available?)
• A note on regular resolution
• A simplified proof that regular resolution is exponential
• Bounds for proof-search and speed-up in the predicate calculus
• On the complexity of regular resolution and the Davis-Putnam procedure
• The relative efficiency of propositional proof systems

Cited in

(21)

• A proper hierarchy of propositional sequent calculi
• Logical structures and genus of proofs
• Gentzen systems, resolution, and literal trees
• Understanding Gentzen and Frege Systems for QBF
• Argumentation in artificial intelligence
• The relative complexity of resolution and cut-free Gentzen systems
• Gentzen-like systems for partial propositional calculi. I. II
• A Fibonacci estimation for the height of Schütte-like cut-free proofs
• Regular Resolution Versus Unrestricted Resolution
• Reduction of Hilbert-type proof systems to the if-then-else equational logic
• An answer to an open problem of Urquhart
• Relative efficiency of a proof system for classical propositional logic
• Proof complexity of substructural logics
• A simulation of natural deduction and Gentzen sequent calculus
• A Gentzen system for conditional logic
• A Logical Autobiography
• Two party immediate response disputes: Properties and efficiency
• The intractability of resolution
• Seventy-five problems for testing automatic theorem provers
• Tractability of cut-free Gentzen type propositional calculus with permutation inference
• A measure of logical inference and its game theoretical applications

This page was built for publication: The complexity of Gentzen systems for propositional logic

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