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

From: <jos.deroo@agfa.com>
Date: Sun, 28 Nov 2004 14:19:53 +0100
To: Yosi Scharf <syosi@mit.edu>

Message-ID: <OF82E9E68D.41A4685B-ONC1256F5A.004614D0-C1256F5A.00495B9E@agfa.com>
```
[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

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:01:04 UTC