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

DOI10.1016/S0304-3975(98)00186-8zbMath0945.03085OpenAlexW2031662653MaRDI QIDQ1575637

Noriko H. Arai

Publication date: 21 August 2000

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

Full work available at URL: https://doi.org/10.1016/s0304-3975(98)00186-8

zbMATH Keywords

computational complexityproof theoryautomated theorem provingrelative efficiencyFrege systemscut-free Gentzen system LK with permutationfeasible subformula propertypermutation inferencerenaming inference

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Complexity of proofs (03F20)

Related Items

No feasible monotone interpolation for simple combinatorial reasoning ⋮ Relative efficiency of propositional proof systems: Resolution vs. cut-free LK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tractability of cut-free Gentzen type propositional calculus with permutation inference
• Functional interpretations of feasibly constructive arithmetic
• Resolution proofs of generalized pigeonhole principles
• The intractability of resolution
• Proof theory. 2nd ed
• Propositional consistency proofs
• A proper hierarchy of propositional sequent calculi
• Some remarks on lengths of propositional proofs
• Cutting planes, connectivity, and threshold logic
• A bounded arithmetic AID for Frege systems
• Polynomial size proofs of the propositional pigeonhole principle
• Lower bounds to the size of constant-depth propositional proofs

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