help checking/reading some proof related to versioning?

I've got a couple proofs that I *think* cwm is producing correctly,
but I'd like to check them with PML tools and/or that javascript
thingy http://www.umsu.de/logik/trees/ .


Dave orchard updated his extensibility/versioning diagram,
and I converted it to RDF/OWL

http://lists.w3.org/Archives/Public/public-xml-versioning/2006Feb/0000.html


http://www.w3.org/2001/tag/2006/ext-vers/
http://www.w3.org/2001/tag/2006/ext-vers/ext-vers-uml
http://www.w3.org/2001/tag/2006/ext-vers/ext-vers-uml.violet
http://www.w3.org/2001/tag/2006/ext-vers/ext-vers-uml.rdf
http://www.w3.org/2001/tag/2006/ext-vers/ext-vers-uml.png

Now I'm working on a theorem about HTML2 and HTML4.
Here's a sketch of the argument:

  1. HTML2 is a sublanguage of HTML4.
  2. a production of chap2 is in HTML2; the intent is chap1in
  3. a consumption of chap2, ?C is in HTML4
  4. Show: ?C intent chap1in
  5. ?C intent chap1in by 1, 2, 3 and defn sublanguage

The defn sublanguage is in 
http://www.w3.org/2001/tag/2006/ext-vers/ext-vers-rules.n3
It includes these 2 rules:

{
  [] ev:text ?TXT; :language [ is :sublanguage of ?BIG ]; :intent ?I.
  ?COMM ev:text ?TXT; :language ?BIG.
} => { ?COMM :intent ?I }.
{
  [] ev:text ?TXT; :language ?BIG; :impact ?I.
  ?COMM ev:text ?TXT; :language [ is :sublanguage of ?BIG ].
} => { ?COMM :impact ?I }.

cwm finds a proof thusly:

2001/tag/2006/ext-vers$ make ex-html24-pf.n3
python ../../../../2000/10/swap/cwm.py ex-html24.n3 ext-vers-rules.n3
--think \
--filter=ex-html24-goal.n3 --why >ex-html24-pf.n3

and it includes promising stuff, such as binding BIG to HTML4:

                             :binding  [
                                 :boundTo  [
                                     n3:uri
"file:/home/connolly/w3ccvs/WWW/2001/tag/2006/ext-vers/ex-html24#HTML4" ];
                                 :variable  [
                                     n3:uri
"file:/home/connolly/w3ccvs/WWW/2001/tag/2006/ext-vers/ext-vers-rules.n3#BIG" ] ],

but I'm not confident I can read it.

I'd like to convert it to PML with
 http://www.w3.org/2000/10/swap/test/reason/to-pml.n3
or a revision thereof.

Another proof I think is working just exploits a cardinality
constraint from the UML diagram:
$ make test-agent-pf.n3
python ../../../../2000/10/swap/cwm.py ext-vers-uml.rdf test-agent.n3 \
owl-excerpt.n3 rdfs-excerpt.n3 --think \
--filter=test-agent-goal.n3  --why >test-agent-pf.n3

and in there we find:

   :gives {tes:a1     = tes:a2 . } 


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

Received on Wednesday, 15 February 2006 04:10:27 UTC