Quantifiers issue
Łukasz Godlewski <[email protected]> Sun, 19 May 2013 20:47:24 +0000
| Newsgroups | gmane.comp.ai.powerloom |
|---|---|
| Message-ID | <[email protected]> |
--===============0859410693==
Content-Type: multipart/alternative;
boundary="_b95a0b2d-9fdc-47ef-b6b2-3c73900ca86f_"
--_b95a0b2d-9fdc-47ef-b6b2-3c73900ca86f_
Content-Type: text/plain; charset="iso-8859-2"
Content-Transfer-Encoding: quoted-printable
Hello All! Firstly I would like to apologize for the style of this e-mail -=
english is not my native language. I want to model such problem in PowerLo=
om (and I have a problem with that):
Firstly I write all necessary code:
(defmodule "LCG" :includes ("PL-USER"))(in-module "LCG")(clear-module "LCG"=
)(reset-features)(in-dialect "KIF")
In our world there are instances of objects named TimeObject:
(defconcept TimeObject)
There are also function named state which returns the instance of TimeObjec=
t from a moment of time (the state of this object in that moment):
(deffunction state ((?o TimeObject) (?time Number)) :-> (?r TimeObject))
Input:o - TimeObjectt - the moment of time (time is digitized)returns: Time=
Object in time t
Lets define a relation (one-argument relation taking TimeObject):
(defrelation foo ((?o TimeObject)) )
Now lets create instances of TimeObject X (basic object X and his 2 states =
in moment 1 and 2):
(assert (TimeObject X))(assert (TimeObject (state X 1)))(assert (TimeObject=
(state X 2)))
All this code works perfect in PowerLoom. Now the most important part of th=
is problem. I would like to tell PowerLoom=2C that if in moment t relation =
foo is fulfilled (is true) then in moment t+1 this is not fulfilled and vic=
e versa=2C so in pseudocode it should looks like:
[FORALL t in 1..n]: foo( state(X=2C t) ) <=3D> not foo( state(X=2C t+1) )wh=
ere state(X=2C t) is a state of object X in moment t.
In PowerLoom I guess it should looks like:
(assert (forall ?t (=3D> (> ?t 0) (<=3D> (foo (state X ?t)) (not (foo (sta=
te X (+ ?t 1)))) ))))
And PowerLoom takes this assertion without any warnings.If I wrote it prope=
rly=2C than for example if in moment 1 foo(X) is true=2C then in moment 2 f=
oo(X) is false=2C in moment 3 foo(X) is true etc.So lets assert that in mom=
ent 1 foo(X) is true:
(assert (foo (state X 1)))
Now if we ask PowerLoom about foo(X) in moment 2:
(ask (foo (state X 2)))
it answers: UNKNOWN.Probably the problem is when we use forall quntfier=2C =
because if we write only this constraint for t=3D1=2C2:(assert (<=3D> (foo=
(state X 1)) (not (foo (state X 2))) ))
then for question: (ask (foo (state X 2))) PowerLoom answers: false as we e=
xpect.
Can you let me know if there are error in PowerLoom or I make a mistake?
Regards=2C=A3ukasz Godlewski
=
--_b95a0b2d-9fdc-47ef-b6b2-3c73900ca86f_
Content-Type: text/html; charset="iso-8859-2"
Content-Transfer-Encoding: quoted-printable
<html>
<head>
<style><!--
.hmmessage P
{
margin:0px=3B
padding:0px
}
body.hmmessage
{
font-size: 12pt=3B
font-family:Calibri
}
--></style></head>
<body class=3D'hmmessage'><div dir=3D'ltr'>Hello All! Firstly I would like =
to apologize for the style of this e-mail - english is not my native langua=
ge. =3B<div>I want to model such problem in PowerLoom (and I have a pro=
blem with that):<div><br></div><div>Firstly I write all necessary code:</di=
v><div><br></div><div><div><font face=3D"Courier New">(defmodule "LCG"</fon=
t></div><div><font face=3D"Courier New"><span class=3D"Apple-tab-span" styl=
e=3D"white-space:pre"> </span>:includes ("PL-USER"))</font></div><div><font=
face=3D"Courier New">(in-module "LCG")</font></div><div><font face=3D"Cour=
ier New">(clear-module "LCG")</font></div><div><font face=3D"Courier New">(=
reset-features)</font></div><div><font face=3D"Courier New">(in-dialect "KI=
F")</font></div></div><div><br></div><div>In our world there are instances =
of objects named TimeObject:</div><div><div><br></div><div><font face=3D"Co=
urier New">(defconcept TimeObject)</font></div></div><div><br></div><div>Th=
ere are also function named state which returns the instance of TimeObject =
from a moment of time (the state of this object in that moment):</div><div>=
<div><br></div><div><font face=3D"Courier New">(deffunction state ((?o Time=
Object) (?time Number)) :->=3B (?r TimeObject))</font></div></div><div><b=
r></div><div>Input:</div><div>o - TimeObject</div><div>t - the moment of ti=
me (time is digitized)</div><div>returns: TimeObject in time t</div><div><b=
r></div><div>Lets define a relation (one-argument relation taking TimeObjec=
t):</div><div><br></div><div><font face=3D"Courier New">(defrelation foo ((=
?o TimeObject)) )</font></div><div><br></div><div>Now lets create instances=
of TimeObject X (basic object X and his 2 states in moment 1 and 2):</div>=
<div><div><br></div><div><font face=3D"Courier New">(assert (TimeObject X))=
</font></div><div><font face=3D"Courier New">(assert (TimeObject (state X 1=
)))</font></div><div><font face=3D"Courier New">(assert (TimeObject (state =
X 2)))</font></div></div><div><br></div><div>All this code works perfect in=
PowerLoom. Now the most important part of this problem. I would like to te=
ll PowerLoom=2C that if in moment t relation foo is fulfilled (is true) the=
n in moment t+1 this is not fulfilled and vice versa=2C so in pseudocode it=
should looks like:</div><div><br></div><div><font face=3D"Courier New">[FO=
RALL t in 1..n]: foo( state(X=2C t) ) <=3B=3D>=3B not foo( state(X=2C t=
+1) )</font></div><div>where state(X=2C t) is a state of object X in moment=
t.</div><div><br></div><div>In PowerLoom I guess it should looks like:</di=
v><div><br></div><div><div><font face=3D"Courier New">(assert (forall ?t (=
=3D>=3B (>=3B ?t 0) (<=3B=3D>=3B =3B</font></div><div><font fac=
e=3D"Courier New"><span class=3D"Apple-tab-span" style=3D"white-space:pre">=
</span>(foo (state X ?t))</font></div><div><font face=3D"Courier New"><spa=
n class=3D"Apple-tab-span" style=3D"white-space:pre"> </span>(not (foo (sta=
te X (+ ?t 1)))) =3B</font></div><div><font face=3D"Courier New">))))</=
font></div></div><div><br></div><div>And PowerLoom takes this assertion wit=
hout any warnings.</div><div>If I wrote it properly=2C than for example if =
in moment 1 foo(X) is true=2C then in moment 2 foo(X) is false=2C in moment=
3 foo(X) is true etc.</div><div>So lets assert that in moment 1 foo(X) is =
true:</div><div><br></div><div><div><font face=3D"Courier New">(assert (foo=
(state X 1)))</font></div></div><div><br></div><div>Now if we ask PowerLoo=
m about foo(X) in moment 2:</div><div><div><br></div><div><font face=3D"Cou=
rier New">(ask (foo (state X 2)))</font></div></div><div><br></div><div>it =
answers: UNKNOWN.</div><div>Probably the problem is when we use forall qunt=
fier=2C because if we write only this constraint for t=3D1=2C2:</div><div><=
div><font face=3D"Courier New">(assert (<=3B=3D>=3B =3B</font></div=
><div><font face=3D"Courier New"><span class=3D"Apple-tab-span" style=3D"wh=
ite-space: pre=3B"> </span>(foo (state X 1))</font></div><div><font face=3D=
"Courier New"><span class=3D"Apple-tab-span" style=3D"white-space: pre=3B">=
</span>(not (foo (state X 2))) =3B</font></div><div><font face=3D"Cour=
ier New">))</font></div></div><div><br></div><div>then for question: (ask (=
foo (state X 2))) PowerLoom answers: false as we expect.</div><div><br></di=
v><div>Can you let me know if there are error in PowerLoom or I make a mist=
ake?</div><div><br></div><div><br></div><div>Regards=2C</div><div>=A3ukasz =
Godlewski</div><div><br></div></div> </div></body>
</html>=
--_b95a0b2d-9fdc-47ef-b6b2-3c73900ca86f_--
--===============0859410693==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
_______________________________________________
powerloom-forum mailing list
[email protected]
http://mailman.isi.edu/mailman/listinfo/powerloom-forum
--===============0859410693==--