Linear time computable problems and first-order descriptions

Abstract

It is well known that every algorithmic problem definable by a formula of first-order logic can be solved in polynomial time, since all these problems are in L (see Aho and Ullman (1979) and Immerman (1987)). Using an old technique of Hanf (Hanf 1965) and other techniques developed to prove the decidability of formal theories in mathematical logic, it is shown that an arbitrary FO -problem over relational structures of bounded degree can be solved in linear time.