Monadic First Order Logic, where all predicates take exactly one argument, is a known decidable fragment of first order logic. Testing whether a formula is satisfiable in this logic is decidable, and there exist resolution-based methods for deciding this.
I'm in a situation where I need to test some monadic first-order logic statements for satisfiability. I realize I will hit theoretical limits for complexity, but I'm hoping I can get reasonable performance in common cases.
Right now, there exist a bunch of theorem provers, which provide fast methods for solving first-order logic problems. These include Vampire, SPASS, E, as well as the quantifier extensions of Z3 and CVC4. However, because of undecidability, they're not guaranteed to halt.
My Question
Of existing theorem provers, are there any who are guaranteed to halt when given a monadic formula as input? Or is there a way to use them to (somewhat) efficiently test monadic formulas for satisfiability?