- From: Dan Connolly <connolly@w3.org>
- Date: Tue, 14 Feb 2006 22:10:20 -0600
- To: public-cwm-talk@w3.org
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