Linear Resolution Principle - First Order Logic

Question

I have a set of clauses S. I know how the Linear Resolution Principle algorithm can find the unsatisfiability of the set , but i dont understand how it finds if the the set is satisfable. How it happens ?

ps: is it somehow connected to the fact that the input resolution algorithm is incomplete ?

It is not completeness: for FOL the Completeness of the Resolution Principle holds: "A set $S$ of clauses is unsatisfiable if and only if there is a deduction of the empty clause from $S$." The issue id about undecidability of FOL: there are formulas that are satisfiable only in infinite domain. — Mauro ALLEGRANZA, Feb 16 '18 at 09:47
Thanks. And how the Linear Resolution Principle proves that a set is satisfable ? If you reply as an answer i can vote you :) — Qwerto, Feb 16 '18 at 10:21
Why, Mauro, the fact that it doesnt produce an empty clause implies that the set is satisfiable ? — Qwerto, Feb 16 '18 at 10:41
You are right Mauro. What i havent clearly understood is the proof of the "completeness of the resolution principle", that is based on the Herbrand Theorem (which i know, thanks to your past explanation of this theorem to me) — Qwerto, Feb 16 '18 at 10:58
There are many versione of the Completeness Th, because there are many proof systems for FOL. But every one must be complete. — Mauro ALLEGRANZA, Feb 16 '18 at 11:09
This is mindblowing. What do you intend for : "many proof systems" ? — Qwerto, Feb 16 '18 at 11:13

score 0 · Accepted Answer · answered Feb 16 '18 at 11:06

It is not completeness.

We have the Completeness of the Resolution Principle:

"A set $S$ of clauses is unsatisfiable if and only if there is a deduction of the empty clause from $S$."

The issue is about undecidability of FOL: there are formulas that are satisfiable only in infinite domains.

When we apply the resolution proof procedure, we have three possible cases: if the procedure halts without producing the empty clause, then the set $S$ is satisfiable. If $S$ is unsatisfiable, the procedure halts with the empty clause.

If, on the other hand, $S$ is satisfiable only in an infinite domain, then the procedure does not halt.

Thus, if we can not deduce the empty clause from $S$, then the set $S$ is not unsatisfiable, i.e. it is satisfiable.

Suppose that we have a set and we use the Resolution Principle many times; at a point no more different clauses are produced. The Resolution Principle then states that the set is satisfiable. But, what the dimostration of this ? (I have understood the "Completeness of the Resolution Principle" , but i havent understood why it works in this case) — Qwerto, Feb 17 '18 at 07:27

Linear Resolution Principle - First Order Logic

1 Answers1

Linked