Loading ...
Sorry, an error occurred while loading the content.

chapter 7 resolution algorithm

Expand Messages
  • Ivan Villanueva
    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
    • 0 Attachment
      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
    • Ivan Villanueva
      ... 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
      • 0 Attachment
        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.