Re: working on "A Model of Authority in the Web"

Very much fun stuff indeed...
Testing with

eye http://www.w3.org/2001/tag/dj9/badmeta.n3 
http://www.w3.org/2001/tag/dj9/speech.n3 
http://www.w3.org/2001/tag/dj9/httpspeech.n3 
http://www.w3.org/2001/tag/dj9/time.n3 
http://www.w3.org/2001/tag/dj9/owl2.n3 
http://www.w3.org/2000/10/swap/util/owlth.n3 
http://www.w3.org/2000/10/swap/util/rdfs-nice.n3 --query 
http://www.w3.org/2001/tag/dj9/contradiction.n3

worked out of the box and spits out a few 100 lines of proof ending with

 r:gives {
  _:sk1 owl:differentFrom _:sk1.
  <http://penguin-house.example/2008/article2> owl:differentFrom <
http://penguin-house.example/2008/article2>.
  <#Bob> owl:differentFrom <#Bob>.
 }].

#ENDS 160 msec


Eye does bnode to univar rewriting in the rule premis and that rewritten 
form is used in the proof..
Apart from that, check.py should now be happy with the proof, be it that 
it is a bit redundant
i.e. up to 518 steps

   * - 518
     - @forSome :_g0 . xx:Bob owl:differentFrom xx:Bob . <
http://penguin-house.example/2008/article2> owl:differentFrom <
http://penguin-house.example/2008/article2> . :_g0 owl:differentFrom :_g0 
.
     - conjoining steps (169, 338, 517)
     - 
 
versus 144 in your http://www.w3.org/2001/tag/dj9/badmeta-pf.html

which I am running right now, but still waiting for a cwm result.. i.e. I 
started
cwm http://www.w3.org/2001/tag/dj9/badmeta.n3 
http://www.w3.org/2001/tag/dj9/speech.n3 
http://www.w3.org/2001/tag/dj9/httpspeech.n3 
http://www.w3.org/2001/tag/dj9/time.n3 
http://www.w3.org/2001/tag/dj9/owl2.n3 
http://www.w3.org/2000/10/swap/util/owlth.n3 
http://www.w3.org/2000/10/swap/util/rdfs-nice.n3 
--solve=http://www.w3.org/2001/tag/dj9/contradiction.n3 --why
more than 40 minutes ago

Kind regards,

Jos De Roo | Agfa HealthCare
Senior Researcher | HE/Advanced Clinical Applications Research
T  +32 3444 7618
 http://www.agfa.com/w3c/jdroo/

Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium
http://www.agfa.com/healthcare



Dan Connolly <connolly@w3.org> 
Sent by: public-cwm-talk-request@w3.org
12/15/2009 07:11 AM

To
public-cwm-talk@w3.org
cc
Jonathan Rees <jar@creativecommons.org>
Subject
Re: working on "A Model of Authority in the Web"







On Mon, 2009-12-14 at 18:03 -0600, Dan Connolly wrote:
> On Mon, 2009-12-14 at 17:44 -0600, Dan Connolly wrote:
> [...]
> > For details on how to run the example through cwm, see
> >   http://www.w3.org/2001/tag/dj9/Makefile
> > 
> > Next step: get cwm to spit out a proof and format
> > it nicely. Wish me luck.
> 
> Sigh. cwm blows chunks. Details attached.

I got it to work by commenting out the assertion;
cwm complains a little bit, but the proof checks.

This is fun stuff...
  http://www.w3.org/2001/tag/dj9/story.html


-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
gpg D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E