Re: A (failing) attempt to get Euler to compute something

Hi, Yosi

I have to spend more time on this, but with simply


@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix math: <http://www.w3.org/2000/10/swap/math#> .
@prefix : <http://yosi.us/math#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .

0 :factorial 1.

{(?x -1) math:sum ?z .
 ?z :factorial ?a .
 (?a ?x) math:product ?y .}
log:implies
{?x :factorial ?y} .


and asking
java Euler factorial.n3 --query q.n3
where q.n3 is

@prefix : <http://yosi.us/math#> .
@prefix q: <http://www.w3.org/2004/ql#>.

[] q:select {6 :factorial ?X}; q:where{6 :factorial ?X} .


we get

# Generated with http://www.agfa.com/w3c/euler/ version R4043 on 25 Nov 
2004 23:58:41 GMT
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

(<file:/temp/factorial.n3>.log:semantics).log:conjunction =>
{
@prefix e: <http://www.agfa.com/w3c/euler/log-rules#>.
@prefix q: <http://www.w3.org/2004/ql#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://yosi.us/math#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.


# Generated with http://www.agfa.com/w3c/euler/ version R4043 on 25 Nov 
2004 23:58:41 GMT
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

(<file:/temp/factorial.n3>.log:semantics).log:conjunction =>
{
@prefix e: <http://www.agfa.com/w3c/euler/log-rules#>.
@prefix q: <http://www.w3.org/2004/ql#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://yosi.us/math#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.

{{
  (6 -1) math:sum 5.
  {
   (5 -1) math:sum 4.
   {
    (4 -1) math:sum 3.
    {
     (3 -1) math:sum 2.
     {
      (2 -1) math:sum 1.
      {
       (1 -1) math:sum 0.
       {0 :factorial 1} e:evidence <file:/temp/factorial.n3#_6>.
       (1 1) math:product 1} => {
      {1 :factorial 1} e:evidence <file:/temp/factorial.n3#_15>}.
      (1 2) math:product 2} => {
     {2 :factorial 2} e:evidence <file:/temp/factorial.n3#_15>}.
     (2 3) math:product 6} => {
    {3 :factorial 6} e:evidence <file:/temp/factorial.n3#_15>}.
    (6 4) math:product 24} => {
   {4 :factorial 24} e:evidence <file:/temp/factorial.n3#_15>}.
   (24 5) math:product 120} => {
  {5 :factorial 120} e:evidence <file:/temp/factorial.n3#_15>}.
  (120 6) math:product 720} => {
 {6 :factorial 720} e:evidence <file:/temp/factorial.n3#_15>}} => {
{_:60_2_3 <http://www.w3.org/2004/ql#select> {6 :factorial 720}} 
e:evidence _:engine_1}.

# Proof found for _:engine_1 in 19 steps (1900000 steps/sec) using 1 
engine (5 triples)
}.


# Proof found for _:engine_1 in 20 steps (499 steps/sec) using 1 engine (0 
triples)
}.


but then
python /w3ccvs/WWW/2000/10/swap/cwm.py factorial.n3 --think --query=q.n3

gives

#Processed by Id: cwm.py,v 1.165 2004/11/19 01:58:39 syosi Exp
        #    using base file:/temp/factorial.n3

#  Notation3 generation by
#       notation3.py,v 1.167 2004/11/23 18:51:32 syosi Exp

#   Base was: file:/temp/factorial.n3

#ENDS


will check this weekend :)



-- 
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/




Yosi Scharf <syosi@mit.edu>
Sent by: public-cwm-talk-request@w3.org
25/11/2004 20:37

 
        To:     Jos De_Roo/AMDUS/MOR/Agfa-NV/BE/BAYER@AGFA
        cc:     public-cwm-talk@w3.org
        Subject:        A (failing) attempt to get Euler to compute something


I was trying out Euler.

 created the attached file (factorial.n3)
running cwm factorial.n3 --think --data --purge gives me

    0     :factorial 1 .

    1     :factorial 1 .

    2     :factorial 2 .

    3     :factorial 6 .

    4     :factorial 24 .

    5     :factorial 120 .

    6     a :Question;
         :factorial 720 .

    720     a :Answer .


I can't figure out how to get Euler to compute factorial for me.
I try
/usr/java/jdk1.5.0/bin/java Euler /home/syosi/program/factorial.n3 
/home/syosi/program/q.n3

and it tells me

# Generated with http://www.agfa.com/w3c/euler/ version R4043 on 25 Nov 
2004 19:35:12 GMT
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

(<file:/home/syosi/program/factorial.n3>.log:semantics).log:conjunction =>
{
# No proof found for file:/home/syosi/program/q.n3 in 123 steps (453 
steps/sec) using 1 engine (7 triples)
}.

No matter what I try, it tells me no proof found. What am I not doing?


Yosi
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix math: <http://www.w3.org/2000/10/swap/math#> .
@prefix : <http://yosi.us/math#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .



{ ?x a :Number;
     math:equalTo 0 . }
log:implies
{?x :factorial 1 . } .



{ ?x a :Number .
(?x -1) math:sum ?z .
 ?z :factorial ?a .
 (?a ?x) math:product ?y .}
log:implies
{?x :factorial ?y} .

{ ?x a :Number .
 (?x -1) math:sum ?z . 
 ?z math:notLessThan 0}
log:implies
{?z a :Number} .

{?x a :Question} log:implies {?x a :Number} .

{?x a :Question;
 :factorial ?y . }
log:implies
{?y a :Answer . } .

:Number a log:Chaff .

6 a :Question .
@prefix : <http://yosi.us/math#> .

_:x a :Answer .

Received on Friday, 26 November 2004 00:09:54 UTC