arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · cs/0702160

A Quantifier-Free String Theory for ALOGTIME Reasoning

François Pitt
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.CC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

François Pitt. 2007-02-28. A Quantifier-Free String Theory for ALOGTIME Reasoning. https://arxiv.org/abs/cs/0702160

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

The Computational Complexity of Holant Problems on 4-regular Graphs from the Stable Subgroup Sequence of $SL(2,\mathbb{C})$

The Holant framework provides a general setting for studying counting problems and includes graph homomorphisms (\#GH) and counting constraint satisfaction problems (\#CSP) as special cases. Over the past twenty years, a series of computational complexity dichotomies have been established for Holant problems, but the classification for complex-valued signatures is still open. The main obstacle is the case in which all signatures have even arity. In this paper, we establish a dichotomy for Holant problems with a complex-valued 4-ary signature, which is a key base case for the full classification of Holant problems. We present a new strategy by introducing Schur's theorem, the classification of finite subgroups of $\mathrm{SL}(2,\mathbb{C})$ and stable subgroup sequences into the proof. These new techniques are of independent interest.

cs.CC↗
arXiv2026

Topology inside NC$^1$

We show that ACC$^0$ is precisely what can be computed with constant-width circuits of polynomial size and polylogarithmic genus. This extends a characterization given by Hansen, showing that planar constant-width circuits also characterize ACC$^0$. Thus polylogarithmic genus provides no additional computational power in this model. We consider other generalizations of planarity, including crossing number and thickness. We show that constant-width circuits of polynomial size and thickness two already suffice to capture all of NC$^1$.

cs.CC↗