Re: querying DAML+OIL syntax

From: Peter F. Patel-Schneider (pfps@research.bell-labs.com)
Date: 11/30/01


Your claimed entailment is not valid.

peter


Problem:

Determine whether 

  (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)

RDFS-entails

  (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 nil)

Solution:

It does not entail.  

Here is part of an rdfs-interpretation for the first RDF graph

	IR = { type unionOf intersectionOf first rest nil
	       X a b c A B C AB AC BC
	       uaibc laibc libc ibc lbc lc
	       iuabubc luabubc uab lubc ubc lab lb }
	IP = { type unionOf intersectionOf first rest }
	IEXT(type)  = { <X,uaibc> <X,ibc> <X,a> <X,b> <X,c> 
		        <A,a> <A, uaibc> <B,b> <C,c>
			<AB,a> <AB,b> <AC,a> <AC,c>
			<BC,b> <BC,c> <BC,ibc> <BC,uaibc>
			... }
	IEXT(unionOf) = { < uaibc laibc > }
	IEXT(intersectionOf)  = { < ibc lbc > }
	IEXT(first)  = { <laibc a> <libc ibc> 
		         <lbc b> <lc c> }
	IEXT(rest)  = { < laibc libc> < libc nil>
		        < lbc lc > <lc nil> }
	IS is the identity map

This interpretation is missing all the built-in RDFS stuff, and some
obvious type relationships, but that does not play here.

This is an RDFS interpretation of the first knowledge base under
the mapping A that maps blanknodes to their id without the ?.  It also
satisfies the semantic requirements on unionOf and intersectionOf, so it is
also a DAML+OIL interpretation of the first knowledge base.

Any mapping that shows that this is an interpretation of the second
knowledge base must include

  ?lbc -> lbc		because of (first ?lbc b)

but then there is no possible mapping for ?ubc because there is no unionOf
pair with lbc as its second element.

QED


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