# Can we verify satisfiability of first order statements via saturation in sub-exponential time?

In first order logic, we can prove satisfiability several ways: Finite model generation, truthful monadic abstractions, and also saturation. With finite model generation techniques, we can verify the model directly. With saturation we saturate the search space, running out of inferences, thus proving that a model exists.

How can we verify satisfiability demonstrated through saturation without rerunning the entire search, which might take quite a long time? Satisfiability demonstrated through saturation might be an infinite model, so model generation may not be sufficient.

• There is a straightforward way to turn a saturation proof into a model, which is at the base of tableau methods. The verification takes time proportional to the depth of the truth tree. See e.g. these slides. – cody Dec 22 '14 at 17:17