Re: Tried to bind * to NULL value.

Hans Chalupsky <[email protected]> Thu, 6 Jan 2011 21:23:39 -0800
Newsgroups gmane.comp.ai.powerloom
Message-ID <[email protected]>
Yes, looks like a bug.  It's probably getting tripped up somewhere in the
normalization of

> (assert (forall (?s1 ?s2) (=> (and (set ?s1) (set ?s2))
>            (<=> (forall (?x) (<=> (member ?x ?s1) (member ?x ?s2))) 
>               (equal ?s1 ?s2)))))

I'd suggest to rewrite the rule into

(assert (forall (?s1 ?s2)
          (=> (and (set ?s1)
                   (set ?s2)
                   (forall (?x) (<=> (member ?x ?s1) (member ?x ?s2))))
              (equal ?s1 ?s2))))

which will allow you to prove (equal A B) with your KB.  You can add the
reverse direction also if you need that:

(assert (forall (?s1 ?s2)
          (=> (and (set ?s1)
                   (set ?s2)
                   (equal ?s1 ?s2))
              (forall (?x) (<=> (member ?x ?s1) (member ?x ?s2))))))

PowerLoom's normalization of complex nested quantification is a bit shakey at
times, since it doesn't do a standard clause-form transformation.
Fixing that has been on the to-do list for a long time but never
bubbled up to the top.  I'll see whether I can fix this once I get out of the
current hole I'm in.

Hans

>>>>> Hans Moser <[email protected]> writes:

> I got "WARNING: Tried to bind |V|?s2 to NULL value.  Potentially a PowerLoom bug". I can't see any error in my code and the negative questio works. 
> Thanks.

> ;;;;
> ;;;; PowerLoom 4.0.0.beta
> ;;;;

> (in-package "STELLA")

> (defmodule "TEST"
>   :documentation "Test module"
>   :includes ("PL-USER"))

> (in-module "TEST")

> (set-feature justifications)

> (defrelation individual (?x))
> (defrelation bounded (?x))
> (defrelation unbounded (?x))
> (defrelation member (?x ?s))
> (defrelation equal (?x ?y))

> (assert (forall (?x) (or (set ?x) (individual ?x))))
> (assert (forall (?x) (or (not (set ?x)) (not (individual ?x)))))

> (assert (forall (?x) (or (bounded ?x) (unbounded ?x))))
> (assert (forall (?x) (or (not (bounded ?x)) (not (unbounded ?x)))))

> (assert (forall (?x ?s) (=> (member ?x ?s) (bounded ?x))))
> (assert (forall (?x ?s) (=> (member ?x ?s) (set ?s))))

> (assert (forall (?x ?y) (=> (equal ?x ?y) (equal ?y ?x))))

> (assert (forall (?s1 ?s2) (=> (and (set ?s1) (set ?s2))
>            (<=> (forall (?x) (<=> (member ?x ?s1) (member ?x ?s2))) 
>               (equal ?s1 ?s2)))))

              
> (assert (set A))
> (assert (set B))
> (assert (individual C))
> (assert (member C A))
> (assert (forall (?m) (=> (member ?m A) (member ?m B))))
> (assert (forall (?m) (=> (member ?m B) (member ?m A))))

> ;;;;
> ;;;;  ERROR?
> ;;;;

> * (ask (equal A B))
> WARNING: Tried to bind |V|?s2 to NULL value.  Potentially a PowerLoom bug

> debugger invoked on a COMMON-LISP:SIMPLE-ERROR:
>   There is no applicable method for the generic function
>     #<COMMON-LISP:STANDARD-GENERIC-FUNCTION COPY (13)>
>   when called with arguments
>     (:NULL_VALUE).

> Type HELP for debugger help, or (SB-EXT:QUIT) to exit from SBCL.

> restarts (invokable by number or by possibly-abbreviated name):
>   0: [ABORT] Exit debugger, returning to top level.

> ((SB-PCL::FAST-METHOD COMMON-LISP:NO-APPLICABLE-METHOD (COMMON-LISP:T))
>  #<unavailable argument>
>  #<unavailable argument>
>  #<COMMON-LISP:STANDARD-GENERIC-FUNCTION COPY (13)>)[:EXTERNAL]
> 0] 0

> * (ask (not (equal A B)))

> FALSE
> *
> * (why)
> 1 (NOT (EQUAL A B))
>     follows by Modus Ponens
>     with substitution {?x/C, ?x/, ?x/, ?x/, ?s2/B, ?s1/A}
>     since 1.1 ! (FORALL (?x1 ?x2)
>                    (<= (NOT (EQUAL ?x1 ?x2))
>                        (AND (SET ?x1)
>                             (SET ?x2)
>                             (OR (EXISTS (?x)
>                                    (AND (MEMBER ?x ?x1)
>                                         (NOT (MEMBER ?x ?x2))))
>                                 (EXISTS (?x)
>                                    (AND (MEMBER ?x ?x2)
>                                         (NOT (MEMBER ?x ?x1))))
>                                 (AND (NOT (EQUAL ?x1 ?x2))
>                                      (FORALL (?x)
>                                         (<= (MEMBER ?x ?x2)
>                                             (MEMBER ?x ?x1)))
>                                      (FORALL (?x)
>                                         (<= (MEMBER ?x ?x1)
>                                             (MEMBER ?x ?x2))))))))
>     and   1.2   (OR (EXISTS (C)
>                        (AND (MEMBER C A)
>                             (NOT (MEMBER C B))))
>                     (EXISTS (?x)
>                        (AND (MEMBER ?x B)
>                             (NOT (MEMBER ?x A))))
>                     (AND (NOT (EQUAL A B))
>                          (FORALL (?x)
>                             (<= (MEMBER ?x B)
>                                 (MEMBER ?x A)))
>                          (FORALL (?x)
>                             (<= (MEMBER ?x A)
>                                 (MEMBER ?x B)))))
>     and   1.3 ! (SET B)
>     and   1.4 ! (SET A)

> 1.2 (OR (EXISTS (C)
>            (AND (MEMBER C A)
>                 (NOT (MEMBER C B))))
>         (EXISTS (?x)
>            (AND (MEMBER ?x B)
>                 (NOT (MEMBER ?x A))))
>         (AND (NOT (EQUAL A B))
>              (FORALL (?x)
>                 (<= (MEMBER ?x B)
>                     (MEMBER ?x A)))
>              (FORALL (?x)
>                 (<= (MEMBER ?x A)
>                     (MEMBER ?x B)))))
>     follows by Or-Introduction
>     since 1.2.1 (EXISTS (C)
>                    (AND (MEMBER C A)
>                         (NOT (MEMBER C B))))

> 1.2.1 (EXISTS (C)
>          (AND (MEMBER C A)
>               (NOT (MEMBER C B))))
>     follows by Existential Introduction
>     since 1.2.1.1 ! (MEMBER C A)
>     and   1.2.1.2   (NOT (MEMBER C B))

> |kv|(<|i|@JUSTIFICATION,|i|@EXPLANATION-INFO> <|i|@PRIMITIVE-STRATEGY,|i|@EXPLAN
ATION-INFO> <|i|@JUSTIFICATION,|i|@EXPLANATION-INFO> <|i|@PRIMITIVE-STRATEGY,|i|
> @EXPLANATION-INFO> <|i|@PRIMITIVE-STRATEGY,|i|@EXPLANATION-INFO> <|i|@JUSTIFICAT
> ION,|i|@EXPLANATION-INFO> <|i|@PRIMITIVE-STRATEGY,|i|@EXPLANATION-INFO> <|i|@JUS
> TIFICATION,|i|@EXPLANATION-INFO>)
> *
> -- 
> Neu: GMX De-Mail - Einfach wie E-Mail, sicher wie ein Brief!  
> Jetzt De-Mail-Adresse reservieren: http://portal.gmx.net/de/go/demail
> _______________________________________________
> powerloom-forum mailing list
> [email protected]
> http://mailman.isi.edu/mailman/listinfo/powerloom-forum