Our main result is about enumeration of first-order queries. We make use of a
quantifier elimination method reducing the general case to the quantifier-free
case. As a special we obtain a new proof of the linear time model checking
algorithm, already obtained in [1]}, [2]}. Both these results were also
obtained using (implicitly or explicitly) a quantifier elimination method. As
our enumeration of quantifier-free query also needs a specific normal form,
we could not reuse the results of [1]}, [2]}. Hence we came up with our
own method which differ in the technical details if not in the main ideas.
