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.

  • 1
    $\begingroup$ 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. $\endgroup$ – cody Dec 22 '14 at 17:17

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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.