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

DOI10.1016/S0304-3975(96)80704-3zbMATH Open0874.03065OpenAlexW4252046485MaRDI QIDQ672046FDOQ672046

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Hard examples for resolution
• The relative efficiency of propositional proof systems
• The intractability of resolution
• The complexity of the pigeonhole principle
• Propositional consistency proofs
• Polynomial size proofs of the propositional pigeonhole principle
• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of Gentzen systems for propositional logic
• 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
• The permutability of rules in the classical inferential calculus
• 2000 Annual Meeting of the Association for Symbolic Logic
• Title not available (Why is that?)
• Quati: an automated tool for proving permutation lemmas
• No feasible monotone interpolation for simple combinatorial reasoning
• Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II

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)