Sorry, an error occurred while loading the content.

## chapter 7 resolution algorithm

Expand Messages
• Hello soulmates, 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
Message 1 of 2 , Sep 5, 2005
Hello soulmates,
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. And on the next page you can read that
"any clause in which two complementary literals appear can be discarded."

I wonder if PL-RESOLVE should just remove all complementary literals and
returns just a clause with the remaining literals.

Iván Villanueva
--
Encrypted mail preferred.
GPG Key Id: 3FDBF85F 2004-10-18 Ivan-Fernando Villanueva Barrio
• ... That is not the case. Sorry. ... Of course not. The resolution rule allows to discard two complementary literals, but not more at one. For example with the
Message 2 of 2 , Sep 7, 2005
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 :-)
Your message has been successfully submitted and would be delivered to recipients shortly.