[FOM] criteria for the existence of infinite models of FO theories

[Mr Jesse Adam Alama]

Claessen and Lillieström's Infinox is an automated theorem proving
system that checks for the absence a finite model of a (finitely
axiomatized) first-order theory.  See their "Automated inference of
finite unsatisfiability":

  http://www.springerlink.com/content/736h84237v285672/

The main idea behind Infinox is to check whether a finitely
axiomatized first-order theory T has a function symbol f for which T
proves that f is injective and f is not surjective (or vice versa) or
a relation symbol R for which T proves that R is irreflexive,
transitive, and serial.

The problem of determining finite unsatisfiability is, by
Trakhtenbrot's theorem, undecidable.  And surely more "lightweight"
conditions can be added to the fixed list that Infinox uses.  If your
work is concrete enough that an automated theorem prover could be
sensibly applied, Infinox is worth a look.

Jesse