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

[some additional results..]

Euler has some least power when it comes down to induction
e.g. when it is given

  0 :successor 1.
  {?x :successor :y. (?y 1) math:sum ?z} => {?y :successor ?z}.

and asked (with -think)

  ?u :successor ?v.

it will not answer with the infinite set of solutions, but just

  0 :successor 1.


When it is explicitly given the set of numbers in the factorial
premises


@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 a :Number.
1 a :Number.
2 a :Number.
3 a :Number.
4 a :Number.
5 a :Number.
6 a :Number.

0 :factorial 1.

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


then

bash .euler http://eulersharp.sourceforge.net/2004/04test/factorial.n3 \
-nope -think \
-query http://eulersharp.sourceforge.net/2004/04test/factorialQ.n3


answers with


<http://eulersharp.sourceforge.net/2004/04test/factorialQ#> q:answer (0 
1). 
<http://eulersharp.sourceforge.net/2004/04test/factorialQ#> q:answer (1 
1). 
<http://eulersharp.sourceforge.net/2004/04test/factorialQ#> q:answer (2 
2). 
<http://eulersharp.sourceforge.net/2004/04test/factorialQ#> q:answer (3 
6). 
<http://eulersharp.sourceforge.net/2004/04test/factorialQ#> q:answer (4 
24). 
<http://eulersharp.sourceforge.net/2004/04test/factorialQ#> q:answer (5 
120). 
<http://eulersharp.sourceforge.net/2004/04test/factorialQ#> q:answer (6 
720). 


which is also the case for

bash .cwm http://eulersharp.sourceforge.net/2004/04test/factorial.n3 \
-think \
-query=http://eulersharp.sourceforge.net/2004/04test/factorialQ.n3


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

PS another example to force least power is having only
the matching of facts in rule premise, and we experiment
with that since a long time (i.e. since owl-rules) and
what we now do
"facts can be expressed as {}=>{:s :p :o} and
{}=>{?S ?P ?O} in a premise only matches facts"
-- http://www.agfa.com/w3c/euler/#R4057 





Jos De_Roo
26/11/2004 01:08


        To:     Yosi Scharf <syosi@mit.edu>@AGFASMTP
        cc:     public-cwm-talk@w3.org
        Subject:        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 Sunday, 28 November 2004 13:20:33 UTC