<p>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 <strong>assuming certain properties were preserved during proof search</strong>.</p>

<p>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 <em>not made</em> 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.</p>

<p>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.</p>

CC BY-SA 3.0
2017-10-13T13:24:15.007Z
2017-10-13T13:24:15.007Z
selig
<p>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.</p>

<p>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. </p>

CC BY-SA 3.0
2014-12-22T17:17:29.970Z
There is a straightforward way to turn a saturation proof into a model, which is at the base of [tableau methods](http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#First-order_logic_tableau). The verification takes time proportional to the depth of the truth tree. See e.g. [these slides](https://staff.fnwi.uva.nl/u.endriss/teaching/ilcs/2006/slides/fol-tableaux.pdf).
cody
<lo.logic><automated-theorem-proving>
Can we verify satisfiability of first order statements via saturation in sub-exponential time?
dezakin
# Can we verify satisfiability of first order statements via saturation in sub-exponential time?

(Asked by: username_0 on 2014-12-19)

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.

**Tags:** lo.logic, automated-theorem-proving
> **Comments:**
> **username_1**: There is a straightforward way to turn a saturation proof into a model, which is at the base of [tableau methods](http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#First-order_logic_tableau). The verification takes time proportional to the depth of the truth tree. See e.g. [these slides](https://staff.fnwi.uva.nl/u.endriss/teaching/ilcs/2006/slides/fol-tableaux.pdf).  

---

## 1 answers

### Answer by username_2 on 2017-10-13. Score: 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.


---

