We present a new normal form for first-order logic over bounded-degree structures which relies on the symmetry of labeled connections between elements of the structure. The key idea is to use vocabularies with only monadic predicate and monadic function symbols -- so called singulary logic [Church]. Our proof is effective and syntactic, not relying on games or other semantic characterizations. Linear-time computability of first-order queries becomes a direct corollary of this result. Included will be a discussion of why these data structures are the appropriate models for physically realizable databases.
[Church, A.] Introduction to Mathematical Logic, Princeton University Press, 1956.
- http://www.haverford.edu/cmsc/slindell/ - A full paper is available from the author's webpage