If S⊆{0,1};* and S′ = {0,1}*\sbS are both recognized within a certain nondeterministic time bound T then, in not much more time, one can write down tautologies An→A′n with unique interpolants In that define S∩{0,1}n; hence, if one can rapidly find unique interpolants, then one can recognize S within deterministic time Tp for some fixed p\s>0. In general, complexity measures for the problem of finding unique interpolants in sentential logic yield new relations between circuit depth and nondeterministic Turing time, as well as between proof length and the complexity of decision procedures of logical theories.
Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity, / D. MUNDICI. - In: ANNALS OF PURE AND APPLIED LOGIC. - ISSN 0168-0072. - STAMPA. - 27:(1984), pp. 265-273. [10.1016/0168-0072(84)90029-0]
Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity,
MUNDICI, DANIELE
1984
Abstract
If S⊆{0,1};* and S′ = {0,1}*\sbS are both recognized within a certain nondeterministic time bound T then, in not much more time, one can write down tautologies An→A′n with unique interpolants In that define S∩{0,1}n; hence, if one can rapidly find unique interpolants, then one can recognize S within deterministic time Tp for some fixed p\s>0. In general, complexity measures for the problem of finding unique interpolants in sentential logic yield new relations between circuit depth and nondeterministic Turing time, as well as between proof length and the complexity of decision procedures of logical theories.I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.