Logic for Computer Scientists/Propositional Logic/Resolution

ResolutionEdit

In this subsection we will develop a calculus for propositional logic. Until now we have a language, i.e. a set of formulae and we have investigated into semantics and some properties of formulae or sets of clauses. Now we will introduce an inference rule, namely the resolution rule, which allows to derive new clauses from given ones.

Definition 10Edit

A clause R is a resolvent of clauses C_1 and C_2, if there is a literal L \in C_1 and \overline{L}\in
C_2 and


R= (C_1 - \{L\} ) \cup (C_2 -\{\overline{L}\})

where \overline{L} = 
\begin{cases} 
\;\;\,\lnot A \; \text{  if }  L = A \\
\;\;\,A \; \text{  if }  L = \lnot A
\end{cases}

Note that there is a special case, if we construct the resolvent out of two literals, i.e. L and \overline{L} can be resolved upon and yield the empty set. This empty resolvent is depicted by the special symbol \square.
\square denotes an unsatisfiable formula. We define a clause set, which contains this empty clause to be unsatisfiable,

In the following we investigate in properties of the resolution rule and the entire calculus. The following Lemma is stating the correctness of one single application of the resolution rule.

Theorem 7Edit

If S is a set of clauses and R a resolvent of C_1,C_2 \in 
S, then S \equiv S \cup \{R\}

Proof: Let \mathcal{A} be an assignment for S; hence it is an assignment for S \equiv S \cup \{R\} as well. Assume \mathcal{A} \models S: hence for all clauses C from S, we have that \mathcal{A} \models C. The resolvent R of C_1 and C_2 looks like:


R= (C_1 - \{L\} ) \cup (C_2 -\{\overline{L}\})

where L\in C_1 and \overline{L} \in C_2. Now there are two cases:

  • \mathcal{A} \models L: From \mathcal{A} \models C_2 and \mathcal{A} \not\models  \overline{L}, we conclude \mathcal{A} \models (C_2  -\{\overline{L}\}) and hence \mathcal{A} \models R.
  • \mathcal{A} \not \models L: From \mathcal{A} \models C_1 we conclude \mathcal{A} \models (C_1   -\{L\}) and hence \mathcal{A} \models R. The opposite direction of the lemma is obvious.

Definition 11Edit

Let S be s set of clauses and

 Res(S) = S \cup \{ R \mid R \text{ is a resolvent of two clauses in }  
S\}

then

Res^0(S)    =  S
Res^{n+1}(S) =  Res(Res^n(S)), n\geq  0
Res^*(S)    =  \bigcup_{n\geq 0} Res^n(S)

If we understand the process of iterating the Res-operator as a procedure for deriving new clauses from a given set, and in particular to derive possibly the empty clause, we have to ask, under which circumstances we get the empty clause, and vice versa, what does it mean if we get it. These properties are investigates in the following two Theorems.

Theorem 8 (Correctness)Edit

Let S be a set of clauses. If \square \in Res^*(S) then S is unsatisfiable.

Proof: From \square \in Res^*(S) we conclude, that \square is obtained by resolution from two clauses C_1 = \{L\} and C_2 =
\{\overline{L}  \}. Hence there is a \exists n \geq 0 such that \square \in Res^n(S) and C_1, C_2 \in Res^n(S) and therefore Res^n(S) is unsatisfiable. From Theorem (resolution-lemma) we conclude that Res^n(S) \equiv S and hence S is unsatisfiable.

Theorem 9 (Completeness)Edit

Let S be a finite set of clauses. If S is unsatisfiable then \square \in Res^*(S).

Proof: Induction over the number n of atomic formulae in S. With n=0 we have S = \{ \square\} and hence \square \in S \subseteq
Res^*(S).

Assume n fixed and for every unsatisfiable set of clauses S with n atomic formulae A_1, \cdots , A_n it holds that \square
\in Res^*(S).

Assume a set of clauses S with atomic formulae A_1, \cdots
,A_n,A_{n+1}. In the following we construct two clause sets S_f and S_t:

  • S_f is received from S by deleting every occurrence of A_{n+1} in a clause and by deleting every clause which contains an occurrence of \lnot A_{n+1}. This transformation obviously corresponds to interpreting the atom A_{n+1} with false,
  • S_t results from a similar transformation, where occurrences of \lnot A_{n+1} and clauses containing A_{n+1} are deleted, hence A_{n+1} is interpreted with true.

Let us show, that both S_f and S_t are unsatisfiable: Assume an assignment \mathcal{A} for the atomic formale \{ A_1, \cdots, A_n\} which is a model for S_f. Hence the assignment  \mathcal{A}'(B) = 
\begin{cases}
\;\;\, \mathcal{A}(B) \; \text { if } B \in \{ A_1, \cdots, A_n\} \\  
\;\;\, false \text{ if }  B = A_{n+1}
\end{cases}
is a model for S, which leads to a contradiction. A similar construction shows that S_t is unsatisfiable. Hence then we can use the induction assumption to conclude that \square \in Res^*(S_t) and \square \in Res^*(S_f). Hence there is a sequence of clauses


C_1, \cdots , C_m = \square

such that \forall 1 \leq i \leq m it holds C_i \in S_f or C_i is a resolvent of two clauses C_a and C_b with a,b < i.There is an analog sequence for S_t:


C_1', \cdots , C_t' = \square

Now we are going to reintroduce the previously deleted literals A_{n+1} and \lnot A_{n+1} in the two sequences:

  • Clause C_i which has been the result of deleting A_{n+1} from the original clause in S are again modified to C_i \cup \{A_n+1\} . This results in a sequence
     \overline{C_1}, \cdots , \overline{ C_m}

where \overline{ C_m} is either \square or A_{n+1}.

  • Analogous we introduce  \lnot A_{n+1} in the second sequence, such that \overline{ C_t'} is either \square or \lnot A_{n+1}

In any of the above cases we get \square \in Res^*(S) latest after one resolution step with \overline{ C_m} and \overline{ C_t'}.


Based on the theorems for correctness and completeness, we give a procedure for deciding the satisfiability of propositional formulae.


Deciding Satisfiability of Propositional Formulae

Given a propositional formula F.

  • Transform F into an equivalent CNF S.
  • Compute Res^n(S) for  n = 0,1,2, \cdots
    • If \square \in Res^n(S) then Stop: unsatisfiable .
    • if  Res^n(S) = Res^{n+1}(S) then Stop: satisfiable .

Theorem 10Edit

If S is a finite set of clauses, then there exists a k \geq 0 such that

Res^k(S) = Res^{k+1}(S)


Until now, we have been dealing with sets of clauses. In the following it will turn out, that it is helpful to talk about sequences of applications of the resolution rule.

Definition 12Edit

A deduction of a clause C from a set of clauses S is a sequence  C_1, \cdots, C_n, such that

  • C_n = C and
  • \forall 1 \leq i \leq n : ( C_i \in S \text{ or }  \exists l,r < i : C_i   \text{ is a resolvent of  }  C_l = and = C_r)


A deduction of the empty clause \square from S is called a refutation of S.


Example We want to show, that the formula  K = ((B \land \lnot A) \lor C) is a logical consequence of F = ( (A \lor (B \lor C)) \land (C \lor \lnot A)). For this negate K and prove the unsatisfiability of  F \land \lnot K

For this you can use the interaction in this book in various forms:

  • Use the interaction Truth Tables for proving the unsatisfiability, or
  • use the interaction CNF Transformation for transforming the formula into CNF, and then
  • use the following interaction Resolution.


ProblemsEdit

Problem 23 (Propositional)Edit

Compute Res^n(M) for all n \geq 0 and Res^*(M) for the following set of clauses:

  1. M = \{\{A\}, \{B\}, \{\lnot A,C\},\{B,\lnot C,\lnot D\}, \{\lnot C,D\},\{\lnot D\}
  2. M = \{\{A,\lnot B\},\{A,B\},\{\lnot A\}\}
  3. M = \{\{A,B,C\},\{\lnot B,\lnot C\},\{\lnot A,C\}\}
  4. M = \{\{\lnot A,\lnot B\},\{B,C\},\{\lnot C,A\}\}

Which formula is satisfiable or which is unsatisfiable?
\Box

Problem 24 (Propositional)Edit

Indicate all resolvent of the clauses in S, where S =\{ \{A, \lnot B, C\}, \{A, B, E\}, \{\lnot A, C, \lnot D\}, \{A, \lnot E\}\}
\Box

Problem 25 (Propositional)Edit

Prove: A resolvent R of two clauses C_1 and C_2 is a logical consequence from C_1 and C_2. Note: Use the definition of "consequence".
\Box

Problem 26 (Propositional)Edit

Let M be a set of formulae and F a formula. Prove:

M \models F iff M \cup \{\lnot F\} is unsatisfiable.


\Box

Problem 27 (Propositional)Edit

Compute Res^n(S) with n = 0, 1, 2 and

S = \{ \{A, \lnot B, C\}, \{B, C\}, A \{\lnot, C\}, \{B, \lnot C\}, \{\lnot C\} \}
\Box

Problem 28 (Propositional)Edit

Show that the following set S of formulae is unsatisfiable, by giving a refutation.
S = (B \lor C \lor D) \land (\lnot C) \land (\lnot B \lor C) \land (B \lor \lnot D)
\Box

Problem 29 (Propositional)Edit

Show by using the resolution rule, that \lnot A \land \lnot B \land C is an inference from the set of clauses F = \{ \{A, C\}, \{\lnot B, \lnot C\}, \{\lnot A\} \}.
\Box

Problem 30 (Propositional)Edit

Show by using the resolution rule, that ((P \to Q \text{ is }) \land P ) \to Q is a tautology.
\Box

Last modified on 1 November 2011, at 13:04