A Proposal for the Web Ontology Language
by Peter F. Patel-Schneider

Abstract

A Web Ontology Language has to have a number of formal pieces, all working together in an effective manner.

Syntax for First-Order Logic

• names
  • p - a collection of names for predicates
  • v - a collection of names for variables
• atomic formulae
  • [<p> <v>*]
• formulae
  • <a>
  • (not <f>)
  • (and <f> <f>)
  • (exists <v> <f>
• statements - formulae with no free variables

Proof Theory for First-Order Logic

• ....

Model Theory for First-Order Logic

• interpretations
  • D - collection of objects - the domain
  • I - mapping from p to sets of sequences of objects
• extended interpretations - add
  • A - mapping from variables to objects
  • an extension of the base interpretation
• an extended interpretation I models a formula
  • [p v1 ... vn] - if < A(v1), ... , A(vn) > in I(p)
  • (not f) - if I does not model f
  • (and f1 f2) - if I models both f1 and f2
  • (exists v f) - if there is some extended interpretation just like I except for its mapping of v that models f

Model Theory for First-Order Logic

• an intepretation models a sentence if there is some extended interpretation that models the sentence
• a sentence entails another if all models of the first are also models of the second

Set Theory

• domain of objects, includes sets of objects
• element-of predicate
• a set consists of the objects that satisfy a predicate
• but what about { x : x not element of x }

Liar's paradox

• domain of objects, includes objects that represent formulae
• special predicate, truth
  • true of an object that represents a formula iff that formula is true
• what about ``This sentence is false''

Datatypes

• collection of datatypes, DT
• a datatype is
  • U(d), URI for the datatype
  • L(d), the lexical space for the datatype
  • V(d), the value space for the datatype
  • LV(d) : L(d) -> V(d), the lexical-to-value mapping for the datatype
• let
  • L = union over d in DT of L(d), lexical values
  • V = union over d in DT of V(d), data values
  • LV = union over d in DT of LV(d)

Syntax

• An OWL-1 Knowledge base is given in the XML XQuery 1.0 data model
• a collection of trees, consisting of nodes
  • element nodes
  • attribute nodes
  • text nodes
  • types for element and attribute nodes from XML Schema
• mapping, Q, that expands qnames

OWL-2 Interpretations

• R, nonempty, disjoint from V, the the domain of resources
• EXT : N -> 2^(Rx(RuV)), property extensions
• CEXT : N -> 2^(RuV), class extensions
• S : N -> R, mapping from URIs to denotation
• A : K -> R u V, mapping from nodes to denotation
• conditions
  • CEXT(rdfs:Resource) = R
  • CEXT(rdfs:Literal) = V
  • d in DT CEXT(U(d)) = Vd
  • CEXT(swol:Thing) = R
  • CEXT(swol:Nothing) = {}

OWL-2 Satisfaction of Class Definitions

• ELEMENT(swol:defineClass,{},<id,desc>)
  • CEXT(Q(id)) = ID(desc)
• ELEMENT(swol:definePrimitiveClass,{},<id,desc>)
  • CEXT(Q(id)) <= ID(desc)
• ELEMENT(swol:disjointWith,{},<id1,id2>)
  • CEXT(Q(id1)) ^ CEXT(Q(id2)) = {}

OWL-2 Satisfaction of Property Definitions

• ELEMENT(swol:samePropertyAs,{},<id1,id2>)
  • EXT(Q(id1)) = EXT(Q(id2))
• ELEMENT(swol:subPropertyOf,{},<id1,id2>)
  • EXT(Q(id1)) <= EXT(Q(id2))
• ELEMENT(swol:domain,{},<id,desc>)
  • EXT(Q(id)) <= ID(desc) x (RuV)
• ELEMENT(swol:range,{},<id,desc>)
  • EXT(Q(id)) <= R x IC(desc)

OWL-2 Satisfaction of Property Definitions

• ELEMENT(swol:ObjectProperty,{},<id>)
  • EXT(Q(id)) <= R x R
• ELEMENT(swol:DatatypeProperty,{},<id>)
  • EXT(Q(id)) <= R x V
• ELEMENT(swol:UniqueProperty,{},<id>)
  • EXT(Q(id)) is functional
• ELEMENT(swol:UnambiguousProperty,{},<id>)
  • converse of EXT(Q(id)) is functional
• ELEMENT(swol:TransitiveProperty,{},<id>)
  • EXT(Q(id)) is transitive

OWL-2 Satisfaction of Object Definitions

• ELEMENT(swol:sameIndividualAs,{},<id1,id2>)
  • S(Q(id1)) in R S(Q(id2)) in R S(Q(id1)) = S(Q(id2))
• ELEMENT(swol:differentIndividualFrom,{},<id1,id2>)
  • S(Q(id1)) in R S(Q(id2)) in R S(Q(id1)) /= S(Q(id2))

OWL-2 Satisfaction of RDF-like Statements

• ELEMENT(name,{propertyAttribute*},{propertyElement*})
  • A(|self|) in CEXT(S(name))

OWL-2 Satisfaction of RDF-like Statements

• ATTRIBUTE(rdf:ID,id)
  • A(|parent|) = S(Q(id))
• ATTRIBUTE(rdf:about,id)
  • A(|parent|) = S(Q(id))
• ATTRIBUTE(name,text,type,value)
  • < A(|parent|) , A(|self|) > in EXT(S(name))
  • A(|self|) = value
• ATTRIBUTE(name,text)
  • < A(|parent|) , A(|self|) > in EXT(S(name))
  • A(|self|) in LV(text)

OWL-2 Satisfaction of RDF-like Statements

• ELEMENT(rdf:type,{},{desc})
  • A(|parent|) in ID(desc)
• ELEMENT(name,{rdf:resource,id},{})
  • < A(|parent|),S(Q(id)) > in IR(name)
• ELEMENT(name,{},{resourceElement})
  • < A(|parent|),S(resourceElement) > in IR(name)
• ELEMENT(name,{},{valueNode=TEXT(text)},type,value)
  • < A(|parent|),A(valueNode) > in IR(name) A(valueNode) = value
• ELEMENT(name,{},{valueNode=TEXT(text)})
  • < A(|parent|),A(valueNode) > in IR(name) A(valueNode) in LV(text)

OWL-2 Extensions for descriptions (ID)

• ELEMENT(id)
  • CEXT(Q(id)) ^ R
• ELEMENT(swol:unionOf,{desc+})
  • ID(desc1) v ... v ID(descn)
• ELEMENT(swol:intersectionOf,{desc+})
  • ID(desc1) ^ ... ^ ID(descn)
• ELEMENT(swol:complementOf,{desc})
  • R \ ID(desc)
• ELEMENT(swol:oneOf,{id*})
  • { S(Q(id1)), ..., S(Q(id1n)) }

OWL-2 Extensions for descriptions (ID)

• ELEMENT(swol:toClass,{},<prop,class>)
  • { x : <x,y> in EXT(prop) implies y in IC(class) }
• ELEMENT(swol:hasValue,{},<prop,id>)
  • { x : <x,S(Q(id))> in EXT(Q(prop)) }
• ELEMENT(swol:hasValue,{},<prop,TEXT(text)>,type,value>)
  • { x : <x,value> in EXT(Q(prop)) }
• ELEMENT(swol:hasClass,{},<prop,class>)
  • { x : exists y <x,y> in EXT(Q(prop)) and y in IC(class) }

OWL-2 Extensions for descriptions (ID)

• ELEMENT(swol:minCardinality,{},<prop,int>)
  • { x : >=int y <x,y> in EXT(Q(prop)) }
• ELEMENT(swol:maxCardinality,{},<prop,int>)
  • { x : <=int y <x,y> in EXT(Q(prop)) }
• ELEMENT(swol:cardinality,{},<prop,int>)
  • { x : =int y <x,y> in EXT(Q(prop)) }

OWL-2 Extensions for descriptions (ID)

• ELEMENT(swol:minCardinality,{},<prop,int,class>)
  • { x : >=int y <x,y> in EXT(Q(prop)) and y in IC(class) }
• ELEMENT(swol:maxCardinality,{},<prop,int,class>)
  • { x : <=int y <x,y> in EXT(Q(prop)) and y in IC(class) }
• ELEMENT(swol:cardinality,{},<prop,int,class>)
  • { x : =int y <x,y> in EXT(Q(prop)) and y in IC(class) }

OWL-2 Extensions for descriptions (IC)

• desc
  • ID(desc)
• ELEMENT(id)
  • L(Q(id))), provided that Q(id) in DT

OWL-2 Models

• An interpretation is a model for an OWL-2 knowledge base if there is some extension of the interpretation that satisfies the knowledge base.
• An OWL-2 knowledge base, KB1, entails another, KB2, if all models of KB1 are also models of KB2.

DAML+OIL Entailment

DAML+OIL Paradox

DAML+OIL mismatch

OWL-1 Entailment