How to do some recursiv inference?
Hans Chalupsky <hans <at> ISI.EDU>
2003-12-19 21:43:51 GMT
Hi Ridwan,
there are a couple of problems going on here.
(1) You need to use the proper quantification in the definition of
`tambah', otherwise the way PowerLoom quantifies the implicitly
quantified variables ?I2 and ?J2 prevents you from getting the
rule you want. I.e., the definition should look like this:
(deffunction tambah ((?I INTEGER) (?J INTEGER)) :-> (?K INTEGER)
:<<= (or (and (= ?I 0) (= ?J ?K))
(exists (?I2 ?J2)
(and (dec ?I ?I2) (inc ?J ?J2) (= (tambah ?I2 ?J2) ?K)))))
(2) In its current default configuration, PowerLoom doesn't back-index
on literals such as numbers or strings. Therefore, it won't find
some of your assertions below which will prevent the inferences
from going through. To make it backindex on literals, you have to
set the variable (in Lisp)
(setq stella::*backlink-all-proposition-arguments?* stella::true)
If you are using Java, you'd have to set the variable
edu.isi.powerloom.logic.$BACKLINK_ALL_PROPOSITION_ARGUMENTSp$
or in C++ the variable
logic::oBACKLINK_ALL_PROPOSITION_ARGUMENTSpo
You can set it in the respective main function or the Lisp top level.
This behavior was motivated by the fact that we wanted to avoid lots of
proposition backpointers from commonly used constants such as 0 or
1, but we might change our position on that for future releases.
(3) There is a bug in variable unbinding that I need to investigate
but that you can work around for now (which causes the "Tried to
bind `|V|?x3' to NULL value..." messages).
That said, here is how you get what you are looking for - this run is in
PowerLoom 3.0 but I don't think it makes a difference for this problem
whether you use 2.0 or 3.0:
STELLA(108): (clear-module pl-user)
:VOID
;;; Tell PowerLoom to backindex on numbers and strings:
STELLA(109): (setq *backlink-all-proposition-arguments?* true)
CL:T
STELLA(110): (defrelation inc(?I ?J))
|r|INC
STELLA(111): (defrelation dec(?I ?J))
|r|DEC
;;; Note the `exists' quantifier different from your original definition:
STELLA(112): (deffunction tambah ((?I INTEGER) (?J INTEGER)) :-> (?K INTEGER)
:<<= (or (and (= ?I 0) (= ?J ?K))
(exists (?I2 ?J2)
(and (dec ?I ?I2) (inc ?J ?J2) (= (tambah ?I2 ?J2) ?K)))))
|f|TAMBAH
STELLA(113): (assert (inc 1 2))
|P|(INC 1 2)
STELLA(114): (assert (inc 0 1))
|P|(INC 0 1)
STELLA(115): (assert (inc 2 3))
|P|(INC 2 3)
STELLA(116): (assert (dec 2 1))
|P|(DEC 2 1)
STELLA(117): (assert (dec 1 0))
|P|(DEC 1 0)
STELLA(118): (assert (dec 3 2))
|P|(DEC 3 2)
;;; trace subgoals so you can see the inferences:
STELLA(119): (set-feature trace-subgoals)
|l|(:TRACE-SUBGOALS :EMIT-THINKING-DOTS :JUST-IN-TIME-INFERENCE)
STELLA(120): (ask (tambah 0 2 2))
PATTERN: []
| GOAL: (= (TAMBAH 0 2) 2)
| | STRATEGY: :ANTECEDENTS
| | RULE: (FORALL (?i ?j ?k)
(<<= (= (TAMBAH ?i ?j) ?k)
(OR (AND (= ?i 0) (= ?j ?k)) (EXISTS (?i2 ?j2)
(AND (DEC ?i ?i2) (INC ?j ?j2) (= (TAMBAH ?i2 ?j2) ?k))))))
| | | GOAL: (OR (AND (= ?i/0 0) (= ?j/2 ?k/2)) (EXISTS (?i2 ?j2)
(AND (DEC ?i/0 ?i2) (INC ?j/2 ?j2) (= (TAMBAH ?i2 ?j2) ?k/2))))
| | | | GOAL: (AND (= ?i/0 0) (= ?j/2 ?k/2))
| | | | | GOAL: (= ?i/0 0)
| | | | | GOAL: (= ?i/0 0)
| | | | | SUCC: ?I=0 ?J=2 ?K=2 truth=T
| | | | | GOAL: (= ?j/2 ?k/2)
| | | | | GOAL: (= ?j/2 ?k/2)
| | | | | SUCC: ?I=0 ?J=2 ?K=2 truth=T
| | | | SUCC: ?I=0 ?J=2 ?K=2 truth=T
| | | SUCC: ?I=0 ?J=2 ?K=2 truth=T
| | SUCC: ?I=0 ?J=2 ?K=2 truth=T
| SUCC: truth=T
TRUE
STELLA(121): (ask (tambah 1 1 2))
PATTERN: []
| GOAL: (= (TAMBAH 1 1) 2)
| | STRATEGY: :ANTECEDENTS
| | RULE: (FORALL (?i ?j ?k)
(<<= (= (TAMBAH ?i ?j) ?k)
(OR (AND (= ?i 0) (= ?j ?k)) (EXISTS (?i2 ?j2)
(AND (DEC ?i ?i2) (INC ?j ?j2) (= (TAMBAH ?i2 ?j2) ?k))))))
| | | GOAL: (OR (AND (= ?i/1 0) (= ?j/1 ?k/2)) (EXISTS (?i2 ?j2)
(AND (DEC ?i/1 ?i2) (INC ?j/1 ?j2) (= (TAMBAH ?i2 ?j2) ?k/2))))
| | | | GOAL: (AND (= ?i/1 0) (= ?j/1 ?k/2))
| | | | | GOAL: (= ?i/1 0)
| | | | | GOAL: (= ?i/1 0)
| | | | | FAIL
| | | | FAIL: truth=U
| | | | GOAL: (EXISTS (?i2 ?j2)
(AND (DEC ?i/1 ?i2) (INC ?j/1 ?j2) (= (TAMBAH ?i2 ?j2) ?k/2)))
| | | | | GOAL: (AND (DEC ?i/1 ?i2) (INC ?j/1 ?j2) (= (TAMBAH ?i2 ?j2) ?k/2))
| | | | | | GOAL: (DEC ?i/1 ?i2)
| | | | | | SUCC: ?I=1 ?J=1 ?K=2 ?I2=0 truth=T
| | | | | | GOAL: (INC ?j/1 ?j2)
| | | | | | SUCC: ?I=1 ?J=1 ?K=2 ?J2=2 ?I2=0 truth=T
| | | | | | GOAL: (= (TAMBAH ?i2/0 ?j2/2) ?k/2)
| | | | | | SUCC: ?I=1 ?J=1 ?K=2 ?J2=2 ?I2=0 truth=T
| | | | | SUCC: ?I=1 ?J=1 ?K=2 ?J2=2 ?I2=0 truth=T
| | | | SUCC: ?I=1 ?J=1 ?K=2 ?J2=2 ?I2=0 truth=T
| | | SUCC: ?I=1 ?J=1 ?K=2 ?J2=2 ?I2=0 truth=T
| | SUCC: ?I=1 ?J=1 ?K=2 ?J2=2 ?I2=0 truth=T
| SUCC: truth=T
TRUE
;;; For retrieval to work we need to work around the unbinding bug for
;;; now which you can do by implementing the OR via two separate rules:
STELLA(122): (deffunction tambah ((?I INTEGER) (?J INTEGER)) :-> (?K INTEGER)
:<<= (and (= ?I 0) (integer ?j) (integer ?k) (= ?J ?K))
:<<= (exists (?I2 ?J2)
(and (dec ?I ?I2) (inc ?J ?J2) (= (tambah ?I2 ?J2) ?K))))
Redefining the `function' named `TAMBAH'
|f|TAMBAH
STELLA(123): (unset-feature trace-subgoals)
|l|(:EMIT-THINKING-DOTS :JUST-IN-TIME-INFERENCE)
;;; Now you can retrieve all solutions:
STELLA(124): (retrieve all (tambah ?x ?y ?z))
There are 6 solutions:
#1: ?X=3, ?Y=0, ?Z=3
#2: ?X=1, ?Y=2, ?Z=3
#3: ?X=1, ?Y=0, ?Z=1
#4: ?X=1, ?Y=1, ?Z=2
#5: ?X=2, ?Y=0, ?Z=2
#6: ?X=2, ?Y=1, ?Z=3
;;; note, that PowerLoom will not try to attempt to enumerate all
;;; integers which would give you the solutions (tambah 0 i i) for
;;; any integer i, but you can ask for their truth value if you
;;; specify a particular i:
STELLA(125): (ask (tambah 0 0 0))
TRUE
STELLA(126): (ask (tambah 0 1 1))
TRUE
STELLA(127): (ask (tambah 0 2 2))
TRUE
STELLA(128): ....
Hans
--------------------------------------------------------------------------
PowerLoom home page: http://www.isi.edu/isd/LOOM/PowerLoom
PowerLoom forum: powerloom-forum <at> isi.edu
PowerLoom request line: powerloom-forum-admin <at> isi.edu
STELLA home page: http://www.isi.edu/isd/LOOM/Stella
--------------------------------------------------------------------------
RSS Feed