Re: need n3 proofs for PML translation test

On Sat, 2007-02-03 at 12:48 -0500, Li Ding wrote:
> Hi Dan,
> 
> can you point me the links to these examples? thanks

Sure. I'm copying public-cwm-talk so Yosi and Jos and
other interested people can see this list of examples
too; I presume you don't mind.

> Socrates

http://www.w3.org/2000/10/swap/test/reason/socrates.n3

to get the proof, run
  python cwm.py socrates.n3 --think --why >soc-pf.n3

see also slides starting with
 http://www.w3.org/2006/09dc-aus/swpf#(15)

> witch

http://www.w3.org/2000/10/swap/test/reason/witch-pf.n3
That's the one we were working on at MIT.
see also
 She's a witch and I have the proof (in N3)
 http://dig.csail.mit.edu/breadcrumbs/node/179

> vegetarian

http://www.w3.org/2000/10/swap/test/reason/conf_reg_ex.n3
http://www.w3.org/2000/10/swap/test/reason/joe_profile.n3

To get the proof, run
  python cwm.py conf_reg_ex.n3 --think --why >,veg-pf.n3
see also slides starting with
 http://www.w3.org/2006/09dc-aus/swpf#(19)

> grddl spec

http://www.w3.org/2004/01/rdxh/grddl-rule-test-pf.n3
( and http://www.w3.org/2004/01/rdxh/grddl-rule-test-pf.txt )

It's 180 steps long, but I think it's actually sorta buggy.
(Yosi, it has the split-bnodes problem, as I recall).

It's built using a Makefile
  http://www.w3.org/2004/01/rdxh/Makefile

especially these two stanzas:
grddl-rule-test-pf.txt: grddl-rule-test-pf.n3
	PYTHONPATH=$(SWAP)/.. $(PYTHON) $(SWAP)/check.py --report grddl-rule-test-pf.n3 >$@


grddl-rule-test-pf.n3: grddl-rule-tests.n3 grddl-rules3.n3 grddl-rule-goal.n3
	$(PYTHON) $(CWM) grddl-rule-tests.n3 grddl-rules3.n3  \
		--think  --filter=grddl-rule-goal.n3 --why >$@

I haven't really written it up, but for context, see the GRDDL spec
  http://www.w3.org/2004/01/rdxh/spec
especially the "mechanical rules" appendix
  http://www.w3.org/2004/01/rdxh/spec#mechspec

> http range-14 proofs 

Hmm... I'm not sure I have actually generated a proof
for this one. I discussed it in...
 playing around with N3, OWL, and inconsistency
 http://lists.w3.org/Archives/Public/public-cwm-talk/2006AprJun/0007

which refer to the paper I gave Deb...
  http://www.w3.org/2006/04/irw65/urisym

I might have run into cwm bugs when generating a proof.
If you get thru the proofs above, let me know and I'll dig into
this one further.

> (owl 1.1 proofs)

I hope to do some of those, but I haven't yet.
For (my) reference, the relevant work in progress is...
 Using ACL2 with Semantic Web Data
 http://dig.csail.mit.edu/2006/Papers/owl-acl2/doc20

> one trip per month

The main file is...
http://www.w3.org/2000/10/swap/test/one_trip_per_month.n3
but it also uses
 http://www.w3.org/2002/12/cal/calAx.n3
and the GRDDL results from my homepage.

It's kinda complicated. Hmm... I seem to have the proof lying
around... ok, it's attached. Ah... and I have the text report
version too. It's 533 steps. I'm not at all sure it's right.

I think it's generated a la:

swap$ python cwm.py
test/one_trip_per_month.n3 ,danc_home.rdf ../../../2002/12/cal/calAx.n3
--think --why >,tripm.n3

where ,danc_home.rdf is the result of running GRDDL on my
homepage. If you get this far and need details, let me know.

See also...
toward "can't be in two places at once" proof with cwm
http://lists.w3.org/Archives/Public/public-cwm-talk/2006JulSep/0011


Another example that comes to mind is the TAG versioning stuff.

http://www.w3.org/2001/tag/2006/ext-vers/ex-html24-pf.n3

See also the containing directory and the Makefile
http://www.w3.org/2001/tag/2006/ext-vers/
http://www.w3.org/2001/tag/2006/ext-vers/Makefile

The write-up is:
  Using RDF and OWL to model language evolution
  http://dig.csail.mit.edu/breadcrumbs/node/87

The whole rules category of my blog is pretty much about
proof.
http://dig.csail.mit.edu/breadcrumbs/taxonomy/term/30

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