- From: Yosi Scharf <syosi@MIT.EDU>
- Date: Mon, 04 Jul 2005 23:03:36 -0400
- To: jos.deroo@agfa.com
- CC: public-cwm-talk@w3.org
>
>
>is getting late and quite hot here, and laptop produces even more with
>
>cwm http://eulersharp.sourceforge.net/2003/03swap/pi-data.n3
> http://eulersharp.sourceforge.net/2003/03swap/pi-rules.n3 --think
> --filter=http://eulersharp.sourceforge.net/2003/03swap/pi-query.n3
>
>actually get http://eulersharp.sourceforge.net/2003/03swap/pi-result.n3
>with euler but am wondering how to change for cwm..
>
>
>--
>Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
>
Looking at pi-rules.n3 ....
>### inference rules for Pi-Calculus
>
>{} => {(?P1 ?P2)!:summation :congruent (?P1 ?P2)!:summation}.
>{} => {(?P1 ?P2)!:summation :congruent (?P2 ?P1)!:summation}.
>{} => {(?P1 (?P2 ?P3)!:summation)!:summation :congruent ((?P1 ?P2)!:summation ?P3)!:summation}.
>
>
Cwm being a forward chainer, it cowardly refuses to reason with an
unbound forAll like we have here. That would be a slightly large amount
of work. For this to work in cwm (or pychinko), you would need the tail
of the rule to say why we want to conclude that {(?P1 ?P2)!:summation
:congruent (?P1 ?P2)!:summation}, such as that {(?P1 ?P2) a :ProcessPair}.
Yosi
Received on Tuesday, 5 July 2005 03:11:45 UTC