# Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?

I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. I realize that some quantified predicate formulas with an arity above 2 are undecidable. But I'm not sure if all of them are provably undecidable. If they are not provably undecidable, then is there an SMT algorithm that can solve quantified n-ary predicate formulas even if sometimes the procedure will not terminate?

Note that for my use case, I'm restricting the model to a finite domain if that helps at all. Yes I'm aware of Trakhtenbrot's theorem.

Sources:

1. Kroening, D., & Strichman, O. (2016). Decision procedures an algorithmic point of view. Springer.
• What do you mean by "all of them are provably undecidable"? Presumably there are some trivial cases that are solvable -- undecidability is about worst-case hardness, not a claim that all instances are hard. What am I missing?
– D.W.
Jan 7 at 20:40
• @D.W. I'm saying that undesirability is used as a reason to use fragments of FOL instead. "all of them" refers to SAT for all formulas accepted by FOL. Jan 7 at 22:06
• Since the bot bumped this question, it might be better asked in Proof Assistants. Jun 7 at 2:37