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

Question

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.

Answer 1

I am assuming by saturation you mean saturation-based reasoning as used by a resolution theorem prover e.g. where we negate and attempt to find a contradiction by saturation if we saturate we can conclude there is no contradiction assuming certain properties were preserved during proof search.

Given this setting, it is the part in bold that kills any attempt to do what you are hoping for. To be able to conclude that a saturated set was produced using a complete proof search procedure means checking every inference not made during proof search to make sure this was allowed. In practice this means looking at selected literals of every given clause and all reductions or deletions.

As far as I'm aware, so far there has been no effort to make theorem provers record the necessary information to check these things. But such information could be exponentially larger than the saturated set.