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.
- Kroening, D., & Strichman, O. (2016). Decision procedures an algorithmic point of view. Springer.