No feasible monotone interpolation for simple combinatorial reasoning

DOI10.1016/S0304-3975(99)00142-5MaRDI QIDQ1575265zbMATH OpenOpenAlexWikidataFDO

Authors 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(99)00142-5

zbMATH Keywords

automated theorem provingCraig's interpolation theoremproof complexityproof theory

Mathematics Subject Classification ID

Review text

The feasible monotone interpolation method has been one of the main tools to prove the exponential lower bounds for relatively weak propositional systems. \textit{N. H. Arai} [Theor. Comput. Sci. 170, No. 1-2, 129-144 (1996; Zbl 0874.03065)] introduced a simple combinatorial reasoning system, GCNF+permutation, as a candidate for an automatizable, though powerful, propositional calculus. We show that the monotone interpolation method is not applicable to prove the superpolynomial lower bounds for Simple Combinatorial Reasoning. At the same time, we show that cutting planes, Hilbert's nullstellensatz and the polynomial calculus do not \(p\)-simulate simple combinatorial reasoning.

Recommendations

• scientific article; zbMATH DE number 1507229
• On Interpolation and Automatization for Frege Systems
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic

Cites work

• A lower bound for the complexity of Craig's interpolants in sentential logic
• scientific article; zbMATH DE number 1263234 (Why is no real title available?)
• scientific article; zbMATH DE number 1114028 (Why is no real title available?)
• scientific article; zbMATH DE number 1142303 (Why is no real title available?)
• scientific article; zbMATH DE number 1507229 (Why is no real title available?)
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Tractability of cut-free Gentzen type propositional calculus with permutation inference
• Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II

Cited in

(4)

• Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
• scientific article; zbMATH DE number 65749 (Why is no real title available?)
• scientific article; zbMATH DE number 1507229 (Why is no real title available?)
• No Efficient Disjunction or Conjunction of Switch-Lists

This page was built for publication: No feasible monotone interpolation for simple combinatorial reasoning

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