Decidable subsets of first-order logic:

One subset of first-order logic that can be decided is if we restrict each of the clauses to be "decreasing," that is, for any instantiation of the variables in the clause, the clause head is a longer string than each of the antecedents of the clause. Then it is easy to see a Prolog-style backward chaining inference can decide any statement in the language, because terms get smaller as it does the resolution.

Another subset is suited to forward-chaining inference. That is where each of the clauses is "increasing," so for any instantiation, the clause head is a shorter string than each of the antecedents. To decide this, you start with a bag containing the initial clauses, and you repeatedly apply the modus ponens rule to produce more clauses which you add to the bag. Eventually, no new clauses can be produced. Then to decide a particular statement, you see if it is a member of the bag.

Fortunately, you can decide a combination of these logics by using currying. You rearrange the antecedents of each clause so that if I1, I2 ... In are increasing with respect to the clause head and D1, D2, ... Dm are decreasing, the clause looks like I1 -> I2 -> ... -> In -> D1 -> D2 -> ... -> Dm -> H. Now the decreasing parts of the clause are part of the new clause head. To use this clause, you would use forward chaining resolution to add the new clause head to the bag, the new clause head being usable with backwards inference.

Partially implemented at http://alkalisoftware.net/resolution.v

So far this gives you forward-backward resolution. A (difficult to implement) extension to backward-forward-backward resolution is achieved by, stepwise, replacing the antecedents of increasing clauses with the new antecedents that could be produced under backward resolution. This step is then combined with forward-backward resolution. For example if you had:

P x -> P (S x)

P (S (S (S x))) -> P x

you could use the first clause to produce:

P (S (S x)) -> P x

P (S x) -> P x

P x -> P x

----

On page 277, the source http://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf states that the E*AE* prefix class of first order logic has exponential finite models.

Proof:

A model of an E*AE* sentence is instantiations for the existential quantifiers, plus Skolem functions f(x), g(x), h(x), for the quantifiers after the universal.

Consider the case where there are monadic functions. Say there is a model U of a sentence phi in the AE* prefix class, i.e. forall x, exists y1 y2 y3, F. The only interesting x's are explicitly named in the formula. Call a value n-remote from x if you have to apply n function symbols in order to reach it. Then it is evident that there are O(|phi|) possible x's in the formula, and that a value can be at most O(|phi|)-remote from x. The number of values referenced can increase by a factor of O(|phi|) at each remove from x.

I also need to cover purely symbolic formulas in x. Pick an unreferenced value * from the model U to serve this purpose. Now restrict the model U to the universe {*, values at most O(|phi|)-remote from x}. What results is a finite model of phi with size O(|phi|^|phi|).
QED.

By JamesCandy