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