Just curious: This monday, I had an exam in Knowledge Processing. They asked what's the problem with FOL (compared to propositional), and I gave the textbook answer that iterating functions gives infinitely many ground terms and makes it undecidable. And since I'm a bigmouth, lavedida, I added that I strongly suspect throwing just that feature out won't suffice. (Cf. e.g. planners like STRIPS, which are far weaker than FOL.)  

We simply let that one go since it was irrelevant for the exam (and neither of us had the math knowledge) but I still want to know: Can you restrict FOL so that you still have quantors (which are the whole point) but the resulting axiom system is decidable?



Restricting First Order Logic to make it decidable
There are various decidable fragments of FOL. Beyond prefix classes which Emil Jeřábek mentioned, other common fragments are:


* Two variable logics. The fragment of FOL in which only two variables x and y are allowed is decidable. There are extensions of this logic which are decidable, e.g. with counting quantifiers $\exists ^{\leq 5} x$. Note that allowing even three variables leads to undecidability.
* Guarded logics. Here all quantification is guarded by a predicate from the signature, e.g. $\forall x,y,z\, (R(x,y,z) \to S(z,z,y,x))$. This remains true with various extensions including that go beyond FOL such as fixed point logic.


If you want to know more, have a look at:
Decidable Fragments of First-Order and Fixed-Point Logic - From prefix vocabulary classes to guarded logics (2003) by Erich Grädel. 
I believe it is unpublished, but you can google a manuscript and slides. 


