Re: Axiomatic Semantics of OWL

Peter: 

It is certainly still necessary for us to develop a translator from OWL 
syntax into the language of the axiomatic theory before the axioms can 
be generally useful.    The axioms are for the Full version of OWL.

I've interspersed some answers to your detailed questions below:


Peter F. Patel-Schneider wrote:

>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 .
>
let me leave out the colon prefixes---

 op Person : Class

>
>Graph 2:
>	ex:John ex:hasParent ex:Susan .
>  
>
                  HasParent(John, Susan)

or , equivalently,

       Holds(hasParent, John, Susan)


>
>Alternatively, how do I translate the following abstract syntax into the
>language of the axiomatization.
>
>Syntax 1:
>	Class( ex:Person ) .
>

  Person :  Class

>Syntax 2:	
>

               

>	ObjectProperty ( ex:hasParent ) .
>
  op hasParent : Property

>	Individual( ex:John type(owl:Thing) value( ex:hasParent ex:Susan ) ) .
>

if i understand this correctly, it is

   op John : Individual

   Type(John, Thing)

   Holds(hasParent, John, Susan)
  

>	Individual( ex:Susan type(owl:Thing) ) .
>
  op Susan :  Individual

  Type(Susan, Thing)

>
>
>Peter F. Patel-Schneider
>Bell Labs Research
>
>
>
>
>  
>