ALOGTIME and a conjecture of S.A. Cook

Usingsequential, machine-independent characterization of theparallel complexity classesAC ^k andNC ^k , we establish the following conjecture of S.A. Cook. There is a free variable equational logicALV with the property thatif f, g are function symbols forALOGTIME computable functions for which f=g is provable inALV, then there are polynomial size Frege proofs for the infinite family {|f=g| _m ⁿ :n, m} of propositional tautologies. Here, the propositional formula |f=g| _m ⁿ expresses the equality off andg on inputs of length at mostn, provided that the function values are of length at mostm. We establish a related result with constant formula-depth polynomial size Frege proofs for a systemAV related to uniformAC ⁰ functions.Part of this research supported by NSF Grant # DCR-860615. Extended abstract of this paper appeared in theIEEE Proc. of Logic in Computer Science, Philadelphia (June 1990).