No feasible monotone interpolation for simple combinatorial reasoning (Q1575265): Difference between revisions
From MaRDI portal
Created claim: Wikidata QID (P12): Q126812394, #quickstatements; #temporary_batch_1719448105926 |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/s0304-3975(99)00142-5 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2075231625 / rank | |||
Normal rank |
Latest revision as of 10:22, 30 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | No feasible monotone interpolation for simple combinatorial reasoning |
scientific article |
Statements
No feasible monotone interpolation for simple combinatorial reasoning (English)
0 references
21 August 2000
0 references
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.
0 references
automated theorem proving
0 references
proof complexity
0 references
Craig's interpolation theorem
0 references
proof theory
0 references
0 references
0 references