Re: Axiomatic Semantics of OWL

From: Richard Waldinger <waldinge@AI.SRI.COM>
Subject: Axiomatic Semantics of OWL
Date: Sun, 17 Oct 2004 21:22:23 -0700

> A validated set of first-order axioms for OWL, with discussion, is 
> available at
> http://www.kestrel.edu/home/projects/DAML/owl/axiomatic.html
>    or
> http://www.ai.sri.com/daml/owl/axiomatic.htm
> 
> Comments are solicited.
> 
> Here is the abstract for the discussion:
> 
> Abstract:
> 
> The constructs of the Web Ontology Language (OWL) have been described in 
> a first-order axiomatic theory 
> <http://www.kestrel.edu/home/projects/DAML/owl/axioms.sw>.   A theorem 
> prover was used to ensure that intended consequences follow from the 
> axioms.  The theorem prover searched for, and failed to find, 
> inconsistencies in the axioms.  Several new consequences of the axioms 
> were discovered by the theorem prover, redundant axioms were eliminated, 
> and other axioms were simplified.  The axiomatic theory of OWL, with a 
> first-order theorem prover, may be used as a reasoner for the Full 
> version of OWL.

I gave the axioms a quick look.  No inconsistencies jumped out at me, but I
had a very hard time figuring out what is going on.

The biggest problem is that there is no definition of how the language of
the axiomatization relates to the OWL language (any variety), and I was
unable to make a guess at this relationship.  I was even unable to
determine which dialect of OWL should be the source of the translation.
Without this information the axiomatic semantics is not particularly
useful.  I have lots of other potential problems with the axiomatization,
but I can't determine whether these are true problems without knowing the
translation.

Here is a very simple example illustrating the difficulty.  How do I
translate the following graphs into the language of the axiomatization?

Graph 1:
	ex:Person rdf:type rdfs:Class .

Graph 2:
	ex:John ex:hasParent ex:Susan .


Alternatively, how do I translate the following abstract syntax into the
language of the axiomatization.

Syntax 1:
	Class( ex:Person ) .
Syntax 2:	
	ObjectProperty ( ex:hasParent ) .
	Individual( ex:John type(owl:Thing) value( ex:hasParent ex:Susan ) ) .
	Individual( ex:Susan type(owl:Thing) ) .



Peter F. Patel-Schneider
Bell Labs Research

Received on Monday, 18 October 2004 13:39:17 UTC