Re: querying DAML+OIL syntax

From: Dan Connolly (
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

It's in other specifications of first/rest, though:

@prefix ed: <>.
@prefix dc: <>.
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 [
  = <>;
  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.

Dan Connolly, W3C

This archive was generated by hypermail 2.1.4 : 04/02/02 EST