Tractability of cut-free Gentzen type propositional calculus with permutation inference

DOI10.1016/S0304-3975(96)80704-3MaRDI QIDQ672046zbMATH OpenOpenAlexFDO

Authors Noriko H. Arai

Publication date 27 February 1997

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

Full work available at URL https://doi.org/10.1016/s0304-3975(96)80704-3

zbMATH Keywords

computational complexityconsistencypermutationrelative efficiencyFrege systemssubformula propertyautomatic reasoningcut-free Gentzen type propositional calculuspigeonhole principlespolynomial size proofs for hard combinatorial problems

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Complexity of proofs (03F20)

Recommendations

• Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II
• Proof Complexity of the Cut-free Calculus of Structures
• scientific article; zbMATH DE number 1507229
• Proof theory
• The complexity of Gentzen systems for propositional logic

Cites work

• scientific article; zbMATH DE number 440478 (Why is no real title available?)
• scientific article; zbMATH DE number 4059391 (Why is no real title available?)
• scientific article; zbMATH DE number 3557241 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• Hard examples for resolution
• Polynomial size proofs of the propositional pigeonhole principle
• Propositional consistency proofs
• The complexity of Gentzen systems for propositional logic
• The complexity of the pigeonhole principle
• The intractability of resolution
• The relative efficiency of propositional proof systems
• Tractability through symmetries in propositional calculus

Cited in

(12)

• Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
• Formula simplification via invariance detection by algebraically indexed types
• Simulating non-prenex cuts in quantified propositional calculus
• Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
• On the Power of Substitution in the Calculus of Structures
• A propositional proof system with quantification over permutations
• 2000 Annual Meeting of the Association for Symbolic Logic
• scientific article; zbMATH DE number 1507229 (Why is no real title available?)
• The permutability of rules in the classical inferential calculus
• No feasible monotone interpolation for simple combinatorial reasoning
• Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II
• Quati: an automated tool for proving permutation lemmas

This page was built for publication: Tractability of cut-free Gentzen type propositional calculus with permutation inference

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