From: Dan Connolly (connolly@w3.org)
Date: 11/30/01
Dan Connolly wrote:
[...]
> Then... let's write these expressions using only 2-place predicates,
> conjunction, and existential quantification. (i.e. in RDF triples)
To check my work, I wrote A and B in RDF/n3:
ex:x a [ ont:unionOf (ex:a [ ont:intersectionOf (ex:b ex:c) ] ) ].
ex:x a [ ont:intersectionOf ( [ont:unionOf (ex:a ex:b)]
[ ont:unionOf (ex:a ex:c)] ) ].
then (put the relevant namespaces on top and) translated
to RDF/xml; see attached. I've got some code that
convers RDF/xml to a KIF dialect; it produced:
------
;; RDF parsed by Id: sax2rdf.py,v 1.15 2001/11/10 23:21:14 connolly Exp
(prefix-kludge "" "http://www.w3.org/2000/10/swap/log#")
(prefix-kludge "ex" "http://example/daml-entailment#")
(prefix-kludge "ont" "http://www.daml.org/2001/03/daml+oil#")
(prefix-kludge "rdf" "http://www.w3.org/1999/02/22-rdf-syntax-ns#")
(exists (?_rdfxg0 ?_rdfxg1 ?_rdfxg2 ?_rdfxg3 ?_rdfxg4 ?_rdfxg5
?_rdfxg6 ?_rdfxg7 ?_rdfxg8 ?_rdfxg9 ?_rdfxg10 ?_rdfxg11 )
(and
(rdf:type ex:x ?_rdfxg1 )
(ont:unionOf ?_rdfxg1 ?_rdfxg3 )
(ont:first ?_rdfxg3 ex:a )
(ont:rest ?_rdfxg3 ?_rdfxg5 )
(ont:first ?_rdfxg5 ?_rdfxg7 )
(ont:intersectionOf ?_rdfxg7 ?_rdfxg9 )
(ont:first ?_rdfxg9 ex:b )
(ont:rest ?_rdfxg9 ?_rdfxg11 )
(ont:first ?_rdfxg11 ex:c )
(ont:rest ?_rdfxg11 ont:nil )
(ont:rest ?_rdfxg5 ont:nil )
)
)
------
> A= ... becomes:
>
> (exists (?uaibc ?liabc ?libc ?ibc ?lbc ?lc)
> (and
> (type X ?uaibc)
> (unionOf ?uaibc ?laibc)
> (first ?laibc a) (rest ?laibc ?libc)
> (first ?libc ?ibc) (rest ?libc nil)
> (intersectionOf ?ibc ?lbc)
> (first ?lbc b)
> (rest ?lbc ?lc)
> (first ?lc c)
> (rest ?lc nil) ))
11 triples. check.
> B= becomes...
>
> (exists (?iabbc ...)
> (and
> (type X ?iuabubc)
> (intersectionOf ?iuabubc ?luabubc)
> (first ?luabubc ?uab) (rest ?luabubc ?lubc)
> (first ?lubc ?ubc) (rest ?lubc nil)
> (unionOf ?uab ?lab)
> (first ?lab a) (rest ?lab ?lb) (first ?lb b) (rest ?lb nil)
> (unionOf ?ubc ?lbc)
> (first ?lbc b) (rest ?lbc ?lc) (first ?lc c) (rest ?lc c)
> ) )
------
;; RDF parsed by Id: sax2rdf.py,v 1.15 2001/11/10 23:21:14 connolly Exp
(prefix-kludge "" "http://www.w3.org/2000/10/swap/log#")
(prefix-kludge "ex" "http://example/daml-entailment#")
(prefix-kludge "ont" "http://www.daml.org/2001/03/daml+oil#")
(prefix-kludge "rdf" "http://www.w3.org/1999/02/22-rdf-syntax-ns#")
(exists (?_rdfxg0 ?_rdfxg1 ?_rdfxg2 ?_rdfxg3 ?_rdfxg4 ?_rdfxg5
?_rdfxg6 ?_rdfxg7 ?_rdfxg8 ?_rdfxg9 ?_rdfxg10 ?_rdfxg11 ?_rdfxg12
?_rdfxg13 ?_rdfxg14 ?_rdfxg15 ?_rdfxg16 ?_rdfxg17 )
(and
(rdf:type ex:x ?_rdfxg1 )
(ont:intersectionOf ?_rdfxg1 ?_rdfxg3 )
(ont:first ?_rdfxg3 ?_rdfxg5 )
(ont:unionOf ?_rdfxg5 ?_rdfxg7 )
(ont:first ?_rdfxg7 ex:a )
(ont:rest ?_rdfxg7 ?_rdfxg9 )
(ont:first ?_rdfxg9 ex:b )
(ont:rest ?_rdfxg9 ont:nil )
(ont:rest ?_rdfxg3 ?_rdfxg11 )
(ont:first ?_rdfxg11 ?_rdfxg13 )
(ont:unionOf ?_rdfxg13 ?_rdfxg15 )
(ont:first ?_rdfxg15 ex:a )
(ont:rest ?_rdfxg15 ?_rdfxg17 )
(ont:first ?_rdfxg17 ex:c )
(ont:rest ?_rdfxg17 ont:nil )
(ont:rest ?_rdfxg11 ont:nil )
)
)
------
16 triples. Check.
[...]
> If ?c2 is ?ibc, blah blah blah and the result
> follows again.
>
> Hence, by proof by cases, QED.
There's a guy in the #rdfig developing a KIF reasoner
that groks this dialect of KIF (i.e. with namespaces).
I wonder if I could get him to check that there's
a straightfoward proof of B from A-with-DAML-axioms.
--
Dan Connolly, W3C http://www.w3.org/People/Connolly/
<!-- Processed by Id: cwm.py,v 1.82 2001/11/15 22:11:23 timbl Exp -->
<!-- using base file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/daml-ent.n3-->
<rdf:RDF xmlns="http://www.w3.org/2000/10/swap/log#"
xmlns:ex="http://example/daml-entailment#"
xmlns:ont="http://www.daml.org/2001/03/daml+oil#"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#">
<rdf:Description rdf:about="http://example/daml-entailment#x">
<rdf:type rdf:parseType="Resource">
<ont:unionOf rdf:parseType="Resource">
<ont:first rdf:resource="http://example/daml-entailment#a"/>
<ont:rest rdf:parseType="Resource">
<ont:first rdf:parseType="Resource">
<ont:intersectionOf rdf:parseType="Resource">
<ont:first rdf:resource="http://example/daml-entailment#b"/>
<ont:rest rdf:parseType="Resource">
<ont:first rdf:resource="http://example/daml-entailment#c"/>
<ont:rest rdf:resource="http://www.daml.org/2001/03/daml+oil#nil"/>
</ont:rest>
</ont:intersectionOf>
</ont:first>
<ont:rest rdf:resource="http://www.daml.org/2001/03/daml+oil#nil"/>
</ont:rest>
</ont:unionOf>
</rdf:type>
</rdf:Description>
</rdf:RDF>
<!-- Processed by Id: cwm.py,v 1.82 2001/11/15 22:11:23 timbl Exp -->
<!-- using base file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/daml-ent-conc.n3-->
<rdf:RDF xmlns="http://www.w3.org/2000/10/swap/log#"
xmlns:ex="http://example/daml-entailment#"
xmlns:ont="http://www.daml.org/2001/03/daml+oil#"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#">
<rdf:Description rdf:about="http://example/daml-entailment#x">
<rdf:type rdf:parseType="Resource">
<ont:intersectionOf rdf:parseType="Resource">
<ont:first rdf:parseType="Resource">
<ont:unionOf rdf:parseType="Resource">
<ont:first rdf:resource="http://example/daml-entailment#a"/>
<ont:rest rdf:parseType="Resource">
<ont:first rdf:resource="http://example/daml-entailment#b"/>
<ont:rest rdf:resource="http://www.daml.org/2001/03/daml+oil#nil"/>
</ont:rest>
</ont:unionOf>
</ont:first>
<ont:rest rdf:parseType="Resource">
<ont:first rdf:parseType="Resource">
<ont:unionOf rdf:parseType="Resource">
<ont:first rdf:resource="http://example/daml-entailment#a"/>
<ont:rest rdf:parseType="Resource">
<ont:first rdf:resource="http://example/daml-entailment#c"/>
<ont:rest rdf:resource="http://www.daml.org/2001/03/daml+oil#nil"/>
</ont:rest>
</ont:unionOf>
</ont:first>
<ont:rest rdf:resource="http://www.daml.org/2001/03/daml+oil#nil"/>
</ont:rest>
</ont:intersectionOf>
</rdf:type>
</rdf:Description>
</rdf:RDF>
This archive was generated by hypermail 2.1.4 : 04/02/02 EST