Re: querying DAML+OIL syntax

From: Dan Connolly ([email protected])
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