This is a simple and inefficient algorithm. It requires a utility function called "RESOLVE2(CL1, CL2)" which returns the final resolvent of two clauses -- this is what we've been using in class, i.e if we resolve
a V -b V c with a V b V -c V d
the result would be
a V d
Note that this is a generalization of the single resolvent your book defines in section 14.1.2
We can define RESOLVE2(CL1, CL2) as follows:
Function Resolve2(Cl1, Cl2)
ret <- { CL2 }
flag = 0
for each symbol in CL1
if the negation of symbol is an element of CL2
then flag = 1 /* something resolved i.e. X with -X or -X with X */
ret = remove negation of symbol from ret
else if symbol is not an element of CL2
then ret <- ret *OR* symbol .
/* note that if symbol is already in CL2 we do nothing *
if flag = 1 and ret = { } then return *EMPTY*
>b>else return ret
Using Resolve2 the algorithm for Resolution is as follows:
FUNCTION PROP-RESOLVE (Clauses, Conclusion) : Boolean
myclauses <- Clauses U negated-conclusion /* negated conclusion in clause
form - could be multiple clauses *.
new <- { }
loop do
for each Ci, Cj in myclauses do
resolvents <- Resolve2 (Ci, Cj)
if resolvents == *EMPTY* then return true
if resolvents are not already in myclauses then
new <- new U resolvents /* note this is set union - i.e. don't add
something that is already there! */
if new = { } then return false
myclauses <- new U myclauses
note that U is set union -- that is