Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity (Q1076669): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
Created claim: Wikidata QID (P12): Q127957473, #quickstatements; #temporary_batch_1722465628192 |
||
(One intermediate revision by one other user not shown) | |||
Property / cites work | |||
Property / cites work: Model theory. / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4068717 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3957950 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3887444 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Riemann's hypothesis and tests for primality / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A lower bound for the complexity of Craig's interpolants in sentential logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3724312 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Every Prime Has a Succinct Certificate / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On uniform circuit complexity / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4138141 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Complexity problems in computational theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Two Familiar Transitive Closure Algorithms Which Admit No Polynomial Time, Sublinear Space Implementations / rank | |||
Normal rank | |||
Property / Wikidata QID | |||
Property / Wikidata QID: Q127957473 / rank | |||
Normal rank |
Latest revision as of 00:41, 1 August 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity |
scientific article |
Statements
Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity (English)
0 references
1984
0 references
In this paper, the author continues his investigation of the relations among the complexities of computations, of circuits, of interpolation formulas, and of formal proofs. Some of the main results are as follows. (i) Consider tautologies \(H\to K\) that have a unique (up to logical equivalence) interpolant J. If \(P\neq NP\cap coNP\), then no deterministic Turing machine M can produce such J in polynomial time in terms of the length of \(H\to K\). (ii) Consider a finitely axiomatized, complete, first order theory \(\Theta\), and let \(\lambda_{\Theta}\) be a function of the lengths of formulas that give upper bounds on the lengths of their proofs. Further, let T be a function giving an upper bound on the time to produce J in (i). Then an upper bound for a decision procedure of \(\Theta\) in terms of a deterministic Turing machine is \(T^ q\circ \lambda^ p_{\Theta}\) for some p,q\(\in \omega\). (iii) Let \(\delta\) be a function of lengths of tautologies of the nature in (i) that gives the lengths of interpolants. Then any \(S\in NP\cap coNP\) can be computed by circuits \(\{\alpha_ n\}\) whose \(depth(\alpha_ n)'s\) do not exceed the bounds \(k\cdot \log \delta (n^ p)\) where \(k,p>0\) depend only on S.
0 references
proof length
0 references
circuit depth
0 references
deterministic Turing machine
0 references
decision procedure
0 references
lengths of interpolants
0 references