1
$\begingroup$

I am studying theoretical computer science and I am in the part about resolution in propositional calculus. I was reading a theorem (and its proof) that propositional resolution is refutation complete, but I could not fill a particular detail.

The theorem is:

Refutational Completeness of Propositional Resolution. The resolution method in propositional calculus is refutation complete, i.e., a set of propositional clauses $S$ is unsatisfiable if and only if the empty clause can be deduced from $S$ by application of the cut rule and the simplification rule.

The sketch of the proof given is:

Proof Sketch.

($\Leftarrow$). By correction we have that if $\square$ is deduced from $S$ then $S$ is unsatisfiable.

($\Rightarrow$). First you need to show that if $S$ is inconsistent and the set of propositional symbols that occur in the clauses of $S$ are $\{p_1, \ldots, p_n \}$, then it is possible to obtain from $S$ by resolution a set of clauses $S'$ such that only the propositional symbols $\{p_1, \ldots, p_{n-1} \}$ occur in $S'$. The proof will then follow by induction on the number of propositional symbols that occur in $S$. Details are left as exercise.

The cut rule and the simplification rule were defined previously as:

Cut Rule. Let $p \lor l_1 \lor \ldots \lor l_n$ and $\lnot p \lor l'_1 \lor \ldots \lor l'_m$ be two propositional clauses. Then the clause $l_1 \lor \ldots \lor l_n \lor l'_1 \lor \ldots l'_m$ is inferred from the two previous ones by the cut rule.

Simplification Rule. Let $p \lor p \lor l_1 \lor \ldots \lor l_n$ be a propositional clause. Then, the clause $p \lor l_1 \lor \ldots \lor l_n$ is inferred from the one before by the simplification rule. Equally, $\lnot p \lor l_1 \lor \ldots \lor l_n$ is inferred from $\lnot p \lor \lnot p \lor l_1 \lor \ldots \lor l_n$ by the simplification rule.

To obtain the set $S'$ from $S$ my idea was to first notice that since $S$ is unsatisfiable, there is at least one propositional symbol $p_i$ such that both $p_i$ and $\lnot p_i$ appear in clauses of $S$. Without loss of generality, we can assume $p_i = p_n$. Then, let $p_n \lor l_1 \lor \ldots \lor l_n$ and $\lnot p_n \lor l'_1 \lor \ldots \lor l'_m$ be two clauses of $S$ and notice that we can apply the cut rule to obtain only $l_1 \lor \ldots l_n \lor l'_1 \lor \ldots l'_m$. We can proceed in this way as many times as necessary and obtain a set $S'$ such that only the propositional symbols $\{p_1, \ldots, p_{n-1}\}$ appear in $S'$.

However, I could not prove that the set $S'$ obtained this way is inconsistent. For instance, if $S = \{p_1 \lor p_2, p_1 \lor \lnot p_2 \}$, then $S' = \{p_1\}$ and I don't see how I can derive $\square$.

What am I missing? How can I fill the details in this proof? Thanks in advance!

$\endgroup$

1 Answer 1

1
$\begingroup$

There is an error in the example: $S = \{p_1 \lor p_2, p_1 \lor \lnot p_2 \}$ is actually satisfiable. Every interpretation $I$ that sends $p_1$ to $true$ actually works.

With this in mind, notice that if $S$ is unsatisfiable, then for every proposition symbol $p_i$ we may have both $p_i$ and $\lnot p_i$ occurring in $S$ or only one of them. Construct the unsatisfiable subset $S_n$ of $S$ that omits the propositional symbols $p_i$ such that only one of $p_i$ or $\lnot p_i$ occur in $S$. For instance, if $S = \{p_1 \lor p_2, p_1 \lor \lnot p_2, \lnot p_1, p_3 \lor p_1 \}$, then $S_n = \{p_1 \lor p_2, p_1 \lor \lnot p_2, \lnot p_1\}$.

We can then proceed as you described, using the cut rule to combine every pair $p \lor l_1 \lor \ldots \lor l_n$ and $\lnot p \lor l'_1 \lor \ldots \lor l'_m$ and replace them by $l_1 \lor \ldots \lor l_n \lor l'_1 \lor \ldots \lor l'_m$. After that we need to apply the simplification rule to the new rules. We can then form the set $S_{n-1}$ that only contains the propositional symbols $\{p_1, \ldots, p_{n-1} \}$ and also satisfies the property that we have both $p_i$ and $\lnot p_i$ occuring in the clauses of $S_{n-1}$, for every $1 \leq i \leq n-1$. This property will allow us to continue this process of eliminating one propositional symbol at a time until we obtain the empty clause $\square$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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