Re: proof language tests with r:binding - question wrt existentials

From: <jos.deroo@agfa.com>
Date: Sun, 18 Jun 2006 03:00:57 +0200

Message-ID: <OF1AE1EF94.95D8ECCD-ONC1257191.0004999A-C1257191.00058CEF@agfa.com>
```
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
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

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

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