W3C home > Mailing lists > Public > public-cwm-talk@w3.org > April to June 2006

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

From: <jos.deroo@agfa.com>
Date: Sun, 18 Jun 2006 03:00:57 +0200
To: connolly@w3.org, public-cwm-talk@w3.org
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
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 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 8 January 2008 14:11:02 GMT