W3C home > Mailing lists > Public > www-archive@w3.org > March 2008

Re: Skolem Euler Machine test results

From: <jos.deroo@agfa.com>
Date: Tue, 1 Apr 2008 00:00:19 +0200
To: jos.deroo@agfa.com
Cc: www-archive@w3.org
Message-ID: <OF1BE2EE08.13FCAC09-ONC125741D.00789BAE-C125741D.0078E053@agfa.com>
cwm in now also happy with the proof for the induction step in Newman's Lemma
http://eulersharp.sourceforge.net/2006/02swap/test014.in

curl http://eulersharp.sourceforge.net/2006/02swap/test014.in | ~/sem | 
~/sem_tape | ~/cwm
% /home/amdus/wopeg/euler/sem_tape.pl compiled 0.01 sec, 18,196 bytes
%     library(error) compiled into error 0.01 sec, 9,676 bytes
%    library(lists) compiled into lists 0.01 sec, 22,872 bytes
%    library(utf8) compiled into utf8 0.00 sec, 8,584 bytes
%   library(url) compiled into url 0.02 sec, 87,604 bytes
%    library(shlib) compiled into shlib 0.00 sec, 11,256 bytes
%   library(readutil) compiled into read_util 0.00 sec, 20,872 bytes
%   library(socket) compiled into socket 0.01 sec, 6,224 bytes
%   library(option) compiled into swi_option 0.00 sec, 7,844 bytes
%   library(base64) compiled into base64 0.00 sec, 9,652 bytes
%  library(http/http_open) compiled into http_open 0.04 sec, 152,936 bytes
% /home/amdus/wopeg/euler/sem.pl compiled 0.05 sec, 210,112 bytes
  % Total    % Received % Xferd  Average Speed   Time    Time     Time 
Current
                                 Dload  Upload   Total   Spent    Left 
Speed
100   678  100   678    0     0   1497      0 --:--:-- --:--:-- --:--:--  
0

% user://1 compiled 0.00 sec, 2,968 bytes

% user://1 compiled 0.00 sec, 25,288 bytes
#Processed by Id: cwm.py,v 1.197 2007/12/13 15:38:39 syosi Exp 
        #    using base file:///home/amdus/acasvn/2006/02swap/
 
#  Notation3 generation by
#       notation3.py,v 1.200 2007/12/11 21:18:08 syosi Exp

#   Base was: file:///home/amdus/acasvn/2006/02swap/
     @prefix : <http://www.w3.org/2000/10/swap/reason#> .
 
      [      a :Conjunction,
                    :Proof;
             :component  [
                 a :Inference;
                 :evidence  (
                 [
                         a :Inference;
                         :evidence  (
                         [
                                 a :Inference;
                                 :evidence  (
                                 [
                                         a :Inference;
                                         :evidence  (
                                         [
                                                 a :Inference;
                                                 :evidence  (
                                                 [
                                                         a :Fact;
                                                         :gives {<#u> <#s> 
<#v> .
                                                        } ] );
                                                 :gives {<#u>     <#e> 
<#v> .
                                                };
                                                 :rule  [
                                                     a :Extraction;
                                                     :because  [
                                                         a :Parsing;
                                                         :source 
<#e_or_rs> ] ] ] );
                                         :gives {<#v>     <#e> <#u> .
                                        };
                                         :rule  [
                                             a :Extraction;
                                             :because  [
                                                 a :Parsing;
                                                 :source <#sym_e> ] ] ] );
                                 :gives {<#v>     <#s> <#u> .
                                };
                                 :rule  [
                                     a :Extraction;
                                     :because  [
                                         a :Parsing;
                                         :source <#e_in_s> ] ] ]
                         [
                                 a :Fact;
                                 :gives {<#u>     <#s> <#w> .
                                } ] );
                         :gives {<#v>     <#s> <#w> .
                        };
                         :rule  [
                             a :Extraction;
                             :because  [
                                 a :Parsing;
                                 :source <#trans_s> ] ] ]
                 [
                         a :Inference;
                         :evidence  (
                         [
                                 a :Inference;
                                 :evidence  (
                                 [
                                         a :Fact;
                                         :gives {<#w>     a <#dom> .
                                        } ] );
                                 :gives {<#w>     <#e> <#w> .
                                };
                                 :rule  [
                                     a :Extraction;
                                     :because  [
                                         a :Parsing;
                                         :source <#ref_e> ] ] ] );
                         :gives {<#w>     <#s> <#w> .
                        };
                         :rule  [
                             a :Extraction;
                             :because  [
                                 a :Parsing;
                                 :source <#e_in_s> ] ] ] );
                 :gives {<#v>     <#s> <#w> .
                <#w>     <#s> <#w> .
                };
                 :rule  [
                     a :Extraction;
                     :because  [
                         a :Parsing;
                         :source <#found> ] ] ],
                     [
                 a :Inference;
                 :evidence  (
                 [
                         a :Inference;
                         :evidence  (
                         [
                                 a :Inference;
                                 :evidence  (
                                 [
                                         a :Fact;
                                         :gives {<#v>     a <#dom> .
                                        } ] );
                                 :gives {<#v>     <#e> <#v> .
                                };
                                 :rule  [
                                     a :Extraction;
                                     :because  [
                                         a :Parsing;
                                         :source <#ref_e> ] ] ] );
                         :gives {<#v>     <#s> <#v> .
                        };
                         :rule  [
                             a :Extraction;
                             :because  [
                                 a :Parsing;
                                 :source <#e_in_s> ] ] ]
                 [
                         a :Inference;
                         :evidence  (
                         [
                                 a :Inference;
                                 :evidence  (
                                 [
                                         a :Inference;
                                         :evidence  (
                                         [
                                                 a :Inference;
                                                 :evidence  (
                                                 [
                                                         a :Fact;
                                                         :gives {<#u> <#s> 
<#w> .
                                                        } ] );
                                                 :gives {<#u>     <#e> 
<#w> .
                                                };
                                                 :rule  [
                                                     a :Extraction;
                                                     :because  [
                                                         a :Parsing;
                                                         :source 
<#e_or_rs> ] ] ] );
                                         :gives {<#w>     <#e> <#u> .
                                        };
                                         :rule  [
                                             a :Extraction;
                                             :because  [
                                                 a :Parsing;
                                                 :source <#sym_e> ] ] ] );
                                 :gives {<#w>     <#s> <#u> .
                                };
                                 :rule  [
                                     a :Extraction;
                                     :because  [
                                         a :Parsing;
                                         :source <#e_in_s> ] ] ]
                         [
                                 a :Fact;
                                 :gives {<#u>     <#s> <#v> .
                                } ] );
                         :gives {<#w>     <#s> <#v> .
                        };
                         :rule  [
                             a :Extraction;
                             :because  [
                                 a :Parsing;
                                 :source <#trans_s> ] ] ] );
                 :gives {<#v>     <#s> <#v> .
                <#w>     <#s> <#v> .
                };
                 :rule  [
                     a :Extraction;
                     :because  [
                         a :Parsing;
                         :source <#found> ] ] ],
                     [
                 a :Inference;
                 :evidence  (
                 [
                         a :Fact;
                         :gives {<#v>     <#s>  [
                             ] .
                        } ]
                 [
                         a :Inference;
                         :evidence  (
                         [
                                 a :Fact;
                                 :gives {<#w>     <#s>  [
                                     ] .
                                } ]
                         [
                                 a :Fact;
                                 :gives {
                                  [      <#s>  [
                                         ] ].
                                } ] );
                         :gives {<#w>     <#s>  [
                             ] .
                        };
                         :rule  [
                             a :Extraction;
                             :because  [
                                 a :Parsing;
                                 :source <#trans_s> ] ] ] );
                 :gives { @forSome <#_g0> .
                <#v>     <#s> <#_g0> .
                <#w>     <#s> <#_g0> .
                };
                 :rule  [
                     a :Extraction;
                     :because  [
                         a :Parsing;
                         :source <#found> ] ] ];
             :gives { @forSome <#_g1> .
            <#v>     <#s> <#v>,
                        <#w>,
                        <#_g1> .
            <#w>     <#s> <#v>,
                        <#w>,
                        <#_g1> .
            } ].
 
#ENDS

check.py not yet..

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




Jos De Roo
03/23/2008 01:24 AM

 
        To:     www-archive@w3.org
        cc: 
        Subject:        Skolem Euler Machine test results

SEM PROVER http://eulersharp.sourceforge.net/2006/02swap/sem.pl
|
SEM CHECKER http://eulersharp.sourceforge.net/2006/02swap/sem_tape.pl
>
http://eulersharp.sourceforge.net/2006/02swap/sem_test.ref
using test script
http://eulersharp.sourceforge.net/2006/02swap/sem_test
Received on Monday, 31 March 2008 22:01:06 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Wednesday, 7 November 2012 14:18:13 GMT