From: Dan Connolly (connolly@w3.org)
Date: 11/30/01
"Peter F. Patel-Schneider" wrote:
>
> OK, lets try a different example where the non-entailment is even more
> obvious.
I like working with these examples; thanks for making
it more and more concrete...
> peter
>
> Problem:
>
> Determine whether
>
> (type X ?ubc)
> (unionOf ?ubc ?lbc)
> (first ?lbc b) (rest ?lbc ?lc)
> (first ?lc c) (rest ?lc nil)
>
> DAML+OIL-entails
>
> (type X ?uabc)
> (unionOf ?uabc ?labc)
> (first ?labc a) (rest ?labc ?lbc)
> (first ?lbc b) (rest ?lbc ?lc)
> (first ?lc c) (rest ?lc nil)
>
> NB: DAML+OIL-entailment is not yet fully defined. Let's just say, for now,
> that a DAML+OIL interpretation is an RDFS interpretation with the obvious
> extra semantic conditions, taken from the DAML+OIL model theory.
I expect the "obvious extra semantic condintions" includes
an axiom of pairs, ala
(forall (?f ?r)
(=> (list ?r) ((exist (?l) (and (first ?l ?f) (rest ?l ?r)))))
Hmm... it seems to be missing from
http://www.ksl.stanford.edu/people/dlm/daml-semantics/kif-axioms-october2001.txt
It's in other specifications of first/rest, though:
@prefix ed: <http://www.w3.org/2000/08/eb58#>.
@prefix dc: <http://purl.org/dc/elements/1.1/>.
"""
The following basic objects must occur in every universe of discourse.
[...]
All finite lists of objects in the universe of discourse.
"""
is ed:excerpt of [
= <http://logic.stanford.edu/kif/dpans.html#Basics>;
dc:title "Knowledge Interchange Format";
dc:date "Thu, 25 Jun 1998 22:31:37 GMT" ].
> Solution:
>
> It does not entail.
>
> There are interpretations that satisfy the first knowledge base where the
> denotation of a is not in any list,
not if we include an axiom of pairs ala the above.
> i.e., the extension of the denotation
> of ``first'' does not contain any pairs whose second element is the
> denotation of ``a''. These interpretations do not satisfy the second
> knowledge base.
>
> QED
--
Dan Connolly, W3C http://www.w3.org/People/Connolly/
This archive was generated by hypermail 2.1.4 : 04/02/02 EST