On Mon, Sep 05, 2005 at 04:27:31PM +0200, Ivan Villanueva wrote:
> on chapter 7, figure 7.13, the PL-RESOLUTION algorithm is proposed with a
> helper function, PL-RESOLVE, that returns the set of all possible
> clauses obtained by resolving two inputs.
> However, on the previous page the resolution rule is described removing
> all complementary literals at one.
That is not the case. Sorry.
> I wonder if PL-RESOLVE should just remove all complementary literals and
> returns just a clause with the remaining literals.
Of course not. The resolution rule allows to discard two complementary literals,
but not more at one.
For example with the two sentences:
~P1,2 | ~P2,1 | B1,1 ~B1,1 | P1,2 | P2,1
one can apply the resolution rule and get:
~P1,2 | ~P2,1 | P1,2 | P2,1
but not an empty clause.
Ivan Villanueva :-)