- From: <jos.deroo@agfa.com>
- Date: Sun, 18 Jun 2006 03:00:57 +0200
- To: connolly@w3.org, public-cwm-talk@w3.org
After tweaking the proof a bit with some @forSome
check.py in now nicely checking
http://eulersharp.sourceforge.net/2006/02swap/socratesE.n3
and same for
http://eulersharp.sourceforge.net/2006/02swap/radlexE.n3
just that it takes 5 min on my laptop and some 220 MB
but the check is really wonderful!
--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Jos De Roo
12/06/2006 22:13
To: Dan Connolly
cc: public-cwm-talk@w3.org
Subject: proof language tests with r:binding - question wrt
existentials
Hi, Dan
I was able to run some tests with r:binding but have a question wrt
existentials
For a proof like http://www.agfa.com/w3c/euler/socratesE.n3
check.py is running fine for a while and then saying
Reading proof from http://www.agfa.com/w3c/euler/socratesE.n3
Length of proof formula: 91
r:Conjunction _g_L19C1 proof of {2}
Conjunction: 2 components
r:Inference _g_L20C15 proof of {Socrates rdf:type _g10}
Warning: variable is identified by nodeId: <_:Man_5_>
r:Extraction _g_L21C5 proof of {Socrates rdf:type _g13}
r:Parsing _g_L21C72
Indexed query works looking in {3} for {Socrates rdf:type
_g13}
about to test if n3Entails({Socrates rdf:type _g13},
{Socrates rdf:type _:Man_5_})
Indexed query works looking in {Socrates rdf:type
_g13} for {Socrates rdf:type _:Man_5_}
Rule {{var:WHO rdf:type var:WHAT} log:implies {var:WHO
rdf:type var:WHAT}} conditions met
Query.py n3Entails ============
seeing if {Socrates rdf:type _:Man_5_} equals {Socrates rdf:type
_g10}
Tempate {Socrates rdf:type _g10} has existentialVariableName
_g10, formula is {Socrates rdf:type _g10} is { @forSome _g10.
Socrates rdf:type _g10 .}.
# testIncludes BUILTIN, 1 terms in template pe _g10}, 2 unmatched,
1 template variables
Query: created with 2 terms. (justone=0, wc={Socrates rdf:type
_:Man_5_})
{Socrates rdf:type _:Man_5_} :: Socrates rdf:type _g10.
{Socrates rdf:type _:Man_5_} :: {Socrates rdf:type
_:Man_5_} log:existentialVariableName _g10.
rdf:type needs to run: set([])
Socrates needs to run: set([])
_g10 needs to run: set([_g10])
setup: 60) short=1, {Socrates rdf:type _:Man_5_}() :: Socrates()
rdf:type() _g10(_g10)?.
log:existentialVariableName needs to run: set([])
{Socrates rdf:type _:Man_5_} needs to run: set([])
_g10 needs to run: set([_g10])
setup: 50) short=0, {Socrates rdf:type _:Man_5_}() :: {Socrates
rdf:type _:Man_5_}()? log:existentialVariableName() _g10(_g10)?.
QUERY2: called 2 terms, 0 bindings {}, (new: {})
60) short=1, {Socrates rdf:type _:Man_5_}() :: Socrates()
rdf:type() _g10(_g10)?.
50) short=0, {Socrates rdf:type _:Man_5_}() :: {Socrates
rdf:type _:Man_5_}()? log:existentialVariableName() _g10(_g10)?.
query iterating with 2 terms, 0 bindings: ; 0 new bindings: .
60) short=1, {Socrates rdf:type _:Man_5_}() :: Socrates()
rdf:type() _g10(_g10)?.
50) short=0, {Socrates rdf:type _:Man_5_}() :: {Socrates
rdf:type _:Man_5_}()? log:existentialVariableName() _g10(_g10)?.
Looking at 60) short=1, {Socrates rdf:type _:Man_5_}() ::
Socrates() rdf:type() _g10(_g10)?.
...with vars() ExQuVars:(_g10)
Searching (S=60) 1 for 60) short=1, {Socrates rdf:type
_:Man_5_}() :: Socrates() rdf:type() _g10(_g10)?.
...checking {Socrates rdf:type _:Man_5_}
nb1 = {_g10: _:Man_5_}
nb = {}
...searchDone, now 80) short=1, {Socrates rdf:type
_:Man_5_}() :: Socrates() rdf:type() _g10(_g10)?.
nbs=[({_g10: _:Man_5_}, {Socrates rdf:type _:Man_5_})]
QUERY2: called 1 terms, 0 bindings {}, (new: {_g10: _:Man_5_})
50) short=0, {Socrates rdf:type _:Man_5_}() :: {Socrates
rdf:type _:Man_5_}()? log:existentialVariableName() _g10(_g10)?.
new binding: _g10 -> _:Man_5_
binding 50) short=0, {Socrates rdf:type _:Man_5_}() ::
{Socrates rdf:type _:Man_5_}()? log:existentialVariableName() _g10(_g10)?.
with {_g10: _:Man_5_}
...searchDone, now 30) short=0, {Socrates rdf:type
_:Man_5_}() :: {Socrates rdf:type _:Man_5_}()?
log:existentialVariableName() _:Man_5_().
...bound becomes 65) short=0, {Socrates rdf:type _:Man_5_}()
:: {Socrates rdf:type _:Man_5_}()? log:existentialVariableName()
_:Man_5_().
query iterating with 1 terms, 0 bindings: ; 1 new bindings:
_g10->_:Man_5_ .
65) short=0, {Socrates rdf:type _:Man_5_}() :: {Socrates
rdf:type _:Man_5_}()? log:existentialVariableName() _:Man_5_().
Looking at 65) short=0, {Socrates rdf:type _:Man_5_}() ::
{Socrates rdf:type _:Man_5_}()? log:existentialVariableName() _:Man_5_().
...with vars() ExQuVars:()
Traceback (most recent call last):
File "/w3ccvs/WWW/2000/10/swap/check.py", line 721, in ?
main(sys.argv)
File "/w3ccvs/WWW/2000/10/swap/check.py", line 666, in main
policy=policy)
File "/w3ccvs/WWW/2000/10/swap/check.py", line 220, in result
g = checkConjunction(r, f, self, policy, level)
File "/w3ccvs/WWW/2000/10/swap/check.py", line 331, in checkConjunction
g1 = checker.result(e, policy, level)
File "/w3ccvs/WWW/2000/10/swap/check.py", line 244, in result
f.unify(g)
File "C:\w3ccvs\WWW\2000\10\swap\llyn.py", line 729, in unify
existentials=Set(), bindings=bindings) # \
File "C:\w3ccvs\WWW\2000\10\swap\query.py", line 660, in n3Entails
justReturn=1, mode="").resolve()
File "C:\w3ccvs\WWW\2000\10\swap\query.py", line 772, in resolve
k = self.matchFormula(self.statements, self.variables,
self._existentialVariables)
File "C:\w3ccvs\WWW\2000\10\swap\query.py", line 1080, in matchFormula
bindings.copy(), nb, evidence = evidence + [reason])
File "C:\w3ccvs\WWW\2000\10\swap\query.py", line 1011, in matchFormula
nbs = item.tryBuiltin(queue, bindings, evidence=evidence)
File "C:\w3ccvs\WWW\2000\10\swap\query.py", line 1435, in tryBuiltin
if pred.eval(subj, obj, BNone, BNone, proof, BNone):
File "C:\w3ccvs\WWW\2000\10\swap\llyn.py", line 1097, in eval
progress('Failed, which is odd. Subj="%s", Obj="%s"' %
subj.debugString(), obj.debugString())
TypeError: not enough arguments for format string
I tried a few things but was loosing
--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Sunday, 18 June 2006 01:04:26 UTC