- 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 UTC