2000

**Abstract:**
The main contribution of this work is the definition of a
quantifier-free string theory $T_1$ suitable for formalizing
$ALOGTIME$ reasoning. After describing $L_1$ -- a new, simple,
algebraic characterization of the complexity class $ALOGTIME$ based on
strings instead of numbers -- the theory $T_1$ is defined (based on
$L_1$ ), and a detailed formal development of $T_1$ is given.

Then, theorems of $T_1$ are shown to translate into families of propositional tautologies that have uniform polysize Frege proofs, $T_1$ is shown to prove the soundness of a particular Frege system $F$, and $F$ is shown to provably $p$-simulate any proof system whose soundness can be proved in $T_1$. Finally, $T_1$ is compared with other theories for $ALOGTIME$ reasoning in the literature.

To our knowledge, this is the first formal theory for $ALOGTIME$ reasoning whose basic objects are strings instead of numbers, and the first quantifier-free theory formalizing $ALOGTIME$ reasoning in which a direct proof of the soundness of some Frege system has been given (in the case of first-order theories, such a proof was first given by Arai for his theory $AID$). Also, the polysize Frege proofs we give for the propositional translations of theorems of $T_1$ are considerably simpler than those for other theories, and so is our proof of the soundness of a particular $F$-system in $T_1$. Together with the simplicity of $T_1$'s recursion schemes, axioms, and rules these facts suggest that $T_1$ is one of the most natural theories available for $ALOGTIME$ reasoning.

**Table of Contents**

1- Introduction - $eF$-systems and $P$ - $F$-systems and $ALOGTIME$ - Overview 2- The String Algebra $L_1$ - Basic definitions - Functions in $L_0$ - Functions in $L_1$ - $L_1$ and F$ALOGTIME$ 3- The Quantifier-Free Theory $T_1$ - Definitions - Developing the theory - Proving the pigeonhole principle in $T_1$ 4- Theorems of $T_1$ Have Polysize $F$-proofs - Length functions - Term formulas - Propositional translations - The simulation result 5- $T_1$ Proves the Soundness of $F$ - Formalizing $F$-systems - Buss's algorithm for the BSVP - Formalizing the BSVP - The soundness proof - Simulation results 6- Related Work - $T_1$ and $AID$ - $T_1$ and $PV$ 7- Conclusion - Summary - Future work A- Details of Proofs in the Formal Development of $T_1$ - Bibliography