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

DOI10.1016/S0304-3975(96)80704-3zbMath0874.03065OpenAlexW4252046485MaRDI QIDQ672046

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)

Related Items

2000 Annual Meeting of the Association for Symbolic Logic ⋮ On the Power of Substitution in the Calculus of Structures ⋮ Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 ⋮ No feasible monotone interpolation for simple combinatorial reasoning ⋮ Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II ⋮ Relative efficiency of propositional proof systems: Resolution vs. cut-free LK ⋮ Formula simplification via invariance detection by algebraically indexed types

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• Propositional consistency proofs
• The complexity of Gentzen systems for propositional logic
• Tractability through symmetries in propositional calculus
• The complexity of the pigeonhole principle
• Polynomial size proofs of the propositional pigeonhole principle
• Hard examples for resolution
• The relative efficiency of propositional proof systems

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