Text search by first order formula I am searching for substrings that satisfy a given first order formula in a moderately sized text. The formula is made out of usual $\wedge, \neg, \exists$ and predicates Equals(x, "some string"), Before(x, y) and similar, where variables are pairs indices denoting substrings.

If the text is $n$ symbols long and the formula contains $k$ quantifiers, then the brute search is $O(n^{2k+2})$. This is quite a bit of time. I ask, is there a way to significantly improve on this?

Many ranges are 'obviously' not worth iterating over, but I don't see a good way to sufficiently restrict the search space, without enumerating all the possible substrings.
The formula's you propose are very reminiscent of the operations of monadic second order logic: position variables, existence letter on position, relative order of positions, boolean operators and position quantification. As you probably know the power of this scheme equals regular languages.

The transformation from MSO to FSA seems to be horrible (negation is complementation, and existential quantification is handled using nondeterminism, hence exponential blow-up for each combination of the two).   

Nevertheless, that gives a very different complexity, linear in $n$, but multiplied by a tower of 2-powers of height $k$.