A Model Theoretic Semantics for DAML-ONT

Richard Fikes

Deborah L McGuinness

Knowledge Systems Laboratory

Computer Science Department

Stanford University

November 7, 2000

Introduction

This document specifies a model-theoretic semantics for the DAML-ONT language by providing a set of first-order logic axioms that can be assumed to hold in any logical theory that is considered to be logically equivalent translation of a DAML-ONT ontology. Our intent is to provide a precise, succinct, and formal description of the relations and constants in DAML-ONT (e.g., complementOf, intersectionOf, Nothing). The axioms provide that description by placing a set of restrictions on the possible interpretations of those relations and constants. The axioms are written in ANSI Knowledge Interchange Format (KIF) (http://logic.stanford.edu/kif/kif.html), which is a proposed ANSI standard.

This document is organized as an augmentation of the DAML-ONT specification (http://www.daml.org/2000/10/daml-ont.daml). Each set of axioms and their associated comments have been added to the specification document immediately following the portion of the specification for which they provide semantics. For example, the axioms providing semantics for the property “complementOf” immediately follow the XML property element that defines “complementOf”.

We have maintained the ordering of the definitions from the original DAML-ONT specification, although that ordering is not optimal for understanding the axioms. In particular, the following terms are used in axioms before they are defined in the document: Class, Property, domain, range, type, List.

Comments are welcome posted to the www-rdf-logic@w3.org distribution list.

DAML-ONT Specification Annotated with KIF Axioms

<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"

xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"

xmlns="http://www.daml.org/2000/10/daml-ont#">

<rdf:Description about="">

<versionInfo>$Id: daml-ont.daml,v 1.2 2000/10/11 06:30:02 connolly Exp $</versionInfo>

</rdf:Description>

<label>Thing</label>

<comment>The most general class in DAML.</comment>

</Class>

%% “Thing” is a Class.

(Class Thing)[1]

%% Every object is an instance of Thing.

(Thing ?x)[2]

<comment>the class with no things in it.</comment>

</Class>

%% “Nothing” is a Class.

(Class Nothing)

%% No object is an instance of Nothing.

(not (Nothing ?x))

<label>disjointWith</label>

<comment>for disjointWith(X, Y) read: X and Y have no members

in common.

</comment>

</Property>

%% “disjointWith” is a property.

(Property disjointWith)

%% Both arguments of disjointWith are classes.

(domain disjointWith Class)

(range disjointWith Class)

%% Classes that are disjointWith have no instances in common, and at least one of the classes has an instance.

(<=> (disjointWith ?c1 ?c2)

(and (exists ?x (or (type ?x ?c1) (type ?x ?c2)))

(not (exists ?x (and (type ?x ?c1) (type ?x ?c2)))))[3]

<label>Disjoint</label>

<comment>for type(L, Disjoint) read: the classes in L are

pairwise disjoint.

i.e. if type(L, Disjoint), and C1 in L and C2 in L, then disjointWith(C1, C2).

</comment>

</Class>

%% A “Disjoint” is a “List”.

(subClassOf Disjoint List)

%% All items in a “Disjoint” list are classes.

(=> (Disjoint ?l) (Item ?c ?l) (Class ?c))[4]

%% The items in a “Disjoint” list are pairwise disjoint.

(=> (Disjoint ?l)

(Item ?c1 ?l)

(Item ?c2 ?l)

(~= ?c1 ?c2)

(DisjointWith ?c1 ?c2))[5]

<label>unionOf</label>

for unionOf(X, Y) read: X is the union of the classes in the list Y;

i.e. if something is in any of the classes in Y, it's in X, and vice versa.

cf OIL OR</comment>

</Property>

%% “unionOf” is a property.

(Property unionOf)

%% The first argument of “unionOf” is a class.

(Domain unionOf Class)

%% The second argument of “unionOf” is a list of classes.

(Range unionOf List)

(=> (unionOf ?c ?l) (item ?x ?l) (Class ?x))

%% The first argument of “unionOf” is the union of the classes in the list that is the second argument of “unionOf”.

(<=> (unionOf ?c1 ?l)

(<=> (type ?x ?c1)

(exists ?c2 (and (item ?c2 ?l) (type ?x ?c2)))))

<label>disjointUnionOf</label>

for disjointUnionOf(X, Y) read: X is the disjoint union of the classes in

the list Y: (a) for any c1 and c2 in Y, disjointWith(c1, c2),

and (b) i.e. if something is in any of the classes in Y, it's

in X, and vice versa.

cf OIL disjoint-covered

</comment>

</Property>

%% “disjointUnionOf” is a property.

(Property disjointUnionOf)

%% The first argument of “disjointUnionOf” is a class.

(Domain disjointUnionOf Class)

%% The second argument of “disjointUnionOf” is a list of classes whose items are pairwise disjoint.

(Range disjointUnionOf Disjoint)

%% A class that is the disjoint union of a list of pairwise disjoint classes is the union of that list.

(<=> (disjointUnionOf ?c ?l) (and (unionOf ?c ?l) (Disjoint ?l)))

for intersectionOf(X, Y) read: X is the intersection of the classes in the list Y;

i.e. if something is in all the classes in Y, then it's in X, and vice versa.

cf OIL AND</comment>

</Property>

%% “intersectionOf” is a property.

(Property intersectionOf)

%% The first argument of “intersectionOf” is a class.

(Domain intersectionOf Class)

%% The second argument of “intersectionOf” is a list of classes.

(Range intersectionOf List)

(=> (intersectionOf ?c ?l) (item ?x ?l) (Class ?x))

%% The first argument of “intersectionOf” is the intersection of the classes in the list that is the second argument of “intersectionOf”.

(<=> (intersectionOf ?c1 ?l)

(<=> (type ?x ?c1)

(forall ?c2 (=> (item ?c2 ?l) (type ?x ?c2 )))))

for complementOf(X, Y) read: X is the complement of Y; if something is in Y,

then it's not in X, and vice versa.

cf OIL NOT</comment>

</Property>

%% “complementOf” is a property.

(Property complementOf)

%% Both arguments of “complementOf” are classes.

(Domain complementOf Class)

(Range complementOf Class)

%% The complement of a class is the class of objects that are not instances of the class.

(<=> (complementOf ?c1 ?c2)

(and (disjointWith ?c1 ?c2)

(forall ?x (or (type ?x ?c1) (type ?x ?c2)))))

%% Note that one could prove from these axioms that Thing is the complement of Nothing.

</Class>

%%”List” is a class.

(Class List)

%% A list is a sequence.

(subClassOf List Seq)

<comment>for oneOf(C, L) read everything in C is one of the

things in L;

This lets us define classes by enumerating the members.

</comment>

</Property>

%% “oneOf” is a property.

(Property oneOf)

%% The first argument of “oneOf” is a class.

(Domain oneOf Class)

%% The second argument of “oneOf” is a list.

(Range oneOf List)

%% “oneOf” enumerates the instances of a class.

(<=> (oneOf ?c ?l) (<=> (type ?x ?c) (item ?x ?l)))

</Class>

%% “Empty” and “Nothing” are the same class.

(asClass Empty Nothing)

%% Note: There is no definition of “asClass” in the spec. Below are a set of proposed axioms for “asClass”.

%% “asClass” is a property.

(Property asClass)

%% Both arguments of “asClass” are classes.

(Domain asClass Class)

(Range asClass Class)

%% “asClass” asserts that two classes are equivalent.

(<=> (asClass ?c1 ?c2) (= ?c1 ?c2))

</Property>

%% “first” is a property.

(Property first)

%% The first argument of “first” is a list.

(Domain first List)

%% The second argument of “first” is the first item on the list that is the first argument of “first”.

(<=> (first ?l ?x) (exists @r (= ?l (listof ?x @r))))[6]

%%Note: DAML-ONT seems to need an equivalent of KIF’s “listof” as part of the language.

</Property>

%% “rest” is a property.

(Property rest)

%% Both arguments of “rest” are lists.

(Domain rest List)

(Range rest List)

%% The second argument of “rest” is the list consisting of all items except the first in the list that is the first argument of “rest”.

(<=> (rest ?l ?r)

(exists (?x @items)

(and (= ?r (listof @items)) (= ?l (listof ?x @items)))))

<comment>for item(L, I) read: I is an item in L; either first(L, I)

or item(R, I) where rest(L, R).</comment>

</Property>

%% “item” is a property.

(Property item)

%% The first argument of “item” is a list.

(Domain item List)

%% “item” is a synonym for “element of” or “member of” for lists.

(<=> (item ?l ?x)

(or (first ?l ?x) (exists ?r (and (rest ?l ?r) (item ?r ?x)))))

<label>cardinality</label>

<comment>for cardinality(P, N) read: P has cardinality N; i.e.

everything x in the domain of P has N things y such that P(x, y).

</comment>

</Property>

%% “cardinality” is a property.

(Property cardinality)

%% The first argument of “cardinality” is a property.

(Domain cardinality Property)

%% The second argument of “cardinality” is a non-negative integer.

(Range cardinality Number)

(=> (cardinality ?p ?n) (and (integer ?n) (not (negative ?n))))[7]

%% A “no-repeats-list” is a list for which no item occurs more than once.

(<=> (no-repeats-list ?l)

(or (= ?l (listof))

(= ?l (listof ?x))

(and (not (item (rest ?l) (first ?l)))

(no-repeats-list (rest ?l)))))

%% A “values-list” is the list of second arguments that a property has for a given first argument. Note that this formulation assumes a finite number of second arguments for a given property and first argument.

(<=> (values-list ?p ?x ?ys)

(and (Property ?p)

(no-repeats-list ?ys)

(forall ?y (<=> (holds ?p ?x ?y) (item ?ys ?y)))))[8]

%% A property has a “cardinality” n when for each first argument it can have n second arguments.

(<=> (cardinality ?p ?n)

(forall ?x (= (length (values-list ?p ?x)) ?n)))[9]

%%Note: DAML-ONT seems to need an equivalent of KIF’s “length” function as part of the language.

<label>maxCardinality</label>

<comment>for maxCardinality(P, N) read: P has maximum cardinality N; i.e.

everything x in the domain of P has at most N things y such that P(x, y).

</comment>

</Property>

%% “maxCardinality” is a property.

(Property maxCardinality)

%% The first argument of “maxCardinality” is a property.

(Domain maxCardinality Property)

%% The second argument of “maxCardinality” is a non-negative integer.

(Range maxCardinality Number)

(=> (maxCardinality ?p ?n) (and (integer ?n) (not (negative ?n))))

%% A property has a “maxCardinality” n when for each first argument it can at most n second arguments.

(<=> (maxCardinality ?p ?n)

(forall ?x (=< (length (values-list ?p ?x)) ?n)))[10]

<comment>for minCardinality(P, N) read: P has minimum cardinality N; i.e.

everything x in the domain of P has at least N things y such that P(x, y).

</comment>

</Property>

%% “minCardinality” is a property.

(Property minCardinality)

%% The first argument of “minCardinality” is a property.

(Domain minCardinality Property)

%% The second argument of “minCardinality” is a non-negative integer.

(Range minCardinality Number)

(=> (minCardinality ?p ?n) (and (integer ?n) (not (negative ?n))))

%% A property has a “minCardinality” n when for each first argument it can at most n second arguments.

(<=> (minCardinality ?p ?n)

(forall ?x (>= (length (values-list ?p ?x)) ?n)))[11]

<comment>for inverseOf(R, S) read: R is the inverse of S; i.e.

if R(x, y) then S(y, x) and vice versa.</comment>

</Property>

%% “inverseOf” is a property.

(Property inverseOf)

%% Both arguments of “inverseOf” are properties.

(Domain inverseOf Property)

(Range inverseOf Property)

%% Properties that are “inverseOf” hold for the same objects but with the arguments in reverse order.

(<=> (inverseOf ?p1 ?p2)

(forall (?x1 ?x2) (<=> (holds ?p1 ?x1 ?x2) (holds ?p2 ?x2 ?x1))))

%% A “TransitiveProperty” is a “Property”.

(subClassOf TransitiveProperty Property)

%% A “TransitiveProperty” is a transitive binary relation.

(<=> (TransitiveProperty ?p)

(forall (?x ?y ?z)

(=> (holds ?p ?x ?y) (holds ?p ?y ?z) (holds ?p ?x ?z))))

<label>UniqueProperty</label>

<comment>compare with maxCardinality=1; e.g. integer successor:

if P is a UniqueProperty, then

if P(x, y) and P(x, z) then y=z.

aka functional.

</comment>

</Class>

%% A “UniqueProperty” is a “Property”.

(subClassOf UniqueProperty Property)

%% A “UniqueProperty” holds for at most one second argument for each first argument.

(<=> (UniqueProperty ?p) (maxCardinality ?p 1))

<label xml:lang="en">UnambiguousProperty</label>

<comment>if P is an UnambiguousProperty, then

if P(x, y) and P(z, y) then x=z.

aka injective.

e.g. if nameOfMonth(m, "Feb")

and nameOfMonth(n, "Feb") then m and n are the same month.

</comment>

</Class>

%% A “UnambiguousProperty” is a “Property”.

(subClassOf UnambiguousProperty Property)

%% An “UnambiguousProperty” holds for at most one first argument for each second argument.

(<=> (UnambiguousProperty ?p)

(forall (?x ?y ?v)

(=> (holds ?p ?x ?v) (holds ?p ?y ?v) (= ?x ?y))))

%% “Restriction” is a Class.

(Class Restriction)

<label>restrictedBy</label>

<comment>for restrictedBy(C, R), read: C is restricted by R; i.e. the

restriction R applies to c;

if onProperty(R, P) and toValue(R, V)

then for every i in C, we have P(i, V).

if onProperty(R, P) and toClass(R, C2)

then for every i in C and for all j, if P(i, j) then type(j, C2).

</comment>

</Property>

%% “restrictedBy” is a property.

(Property restrictedBy)

%% The first argument of restrictedBy is a class.

(domain restrictedBy Class)

%% The second argument of restrictedBy is a restriction.

(range restrictedBy Restriction)

<comment>for onProperty(R, P), read:

R is a restriction/qualification on P.</comment>

</Property>

%% “onProperty” is a property.

(Property onProperty)

%% The first argument of onProperty is a restriction or a qualification.

(=> (onProperty ?rq ?p) (or (Restriction ?rq) (Qualification ?rq)))

%% The second argument of onProperty is a property.

(range onProperty Property)

<comment>for toValue(R, V), read: R is a restriction to V.</comment>

</Property>

%% “toValue” is a property.

(Property toValue)

%% The first argument of toValue is a restriction.

(domain toValue Restriction)

%% Note: We are assuming the range restriction given above for toValue is wrong and that anything can be the second argument of toValue. In fact one typical use of toValue is with an individual.

%% A “toValue” restriction on a property on a class means that every instance of the class has the second argument of “toValue” as a value of that property.

(=> (restrictedBy ?c ?r) (onProperty ?r ?p) (toValue ?r ?v)

(=> (type ?i ?c) (holds ?p ?i ?v)))

<comment>for toClass(R, C), read: R is a restriction to C.</comment>

</Property>

%% “toClass” is a property.

(Property toClass)

%% The first argument of toClass is a restriction.

(domain toClass Restriction)

%% The second argument of toClass is a class.

(range toClass Class)

%% A “toClass” restriction on a property on a class means that if an instance of the class has a value for that property, then that value must be an instance of the class that is the second argument of “toClass”.

(=> (restrictedBy ?c1 ?r) (onProperty ?r ?p) (toClass ?r ?c2)

(=> (type ?i ?c1) (holds ?p ?i ?v) (type ?v ?c2))

%% “Qualification” is a Class.

(Class Qualification)

<label>qualifiedBy</label>

<comment>for qualifiedBy(C, Q), read: C is qualified by Q; i.e. the

qualification Q applies to C;

if onProperty(Q, P) and hasValue(Q, C2)

then for every i in C, there is some V

so that type(V, C2) and P(i, V).

</comment>

</Property>

%% “qualifiedBy” is a property.

(Property qualifiedBy)

%% The first argument of qualifiedBy is a class.

(domain qualifiedBy Class)

%% The second argument of qualifiedBy is a qualification.

(range qualifiedBy Qualification)

<label>hasValue</label>

<comment>for hasValue(Q, C), read: Q is a hasValue

qualification to C.</comment>

</Property>

%% “hasValue” is a property.

(Property hasValue)

%% The first argument of hasValue is a qualification.

(domain hasValue Qualification)

%% The second argument of hasValue is a class.

(range hasValue Class)

%% A “hasValue” qualification on a property on a class means that each instance of the class has a value for that property that is an instance of the class that is the second argument of “hasValue”.

(=> (qualifiedBy ?c1 ?q) (onProperty ?q ?p) (hasValue ?q ?c2)

(=> (type ?i ?c1)

(exists ?v (and (holds ?p ?i ?v) (type ?v ?c2)))))

%% Note: This implies a minimum cardinality of 1 on ?i’s ?p .

<label>Ontology</label>

<comment>An Ontology is a document that describes

a vocabulary of terms for communication between

(human and) automated agents.

</comment>

</Class>

%% An ontology is a class.

(Class Ontology)

<label>versionInfo</label>

<comment>generally, a string giving information about this

version; e.g. RCS/CVS keywords

</comment>

</Property>

%% “versionInfo” is a property.

(Property versionInfo)

%% The first argument of “versionInfo” is an ontology.

(Domain versionInfo Ontology)

<label>imports</label>

<comment>for imports(X, Y) read: X imports Y;

i.e. X asserts the* contents of Y by reference;

i.e. if imports(X, Y) and you believe X and Y says something,

then you should believe it.

Note: "the contents" is, in the general case,

an ill-formed definite description. Different

interactions with a resource may expose contents

that vary with time, data format, preferred language,

requestor credentials, etc. So for "the contents",

read "any contents".

</comment>

</Property>

%% “imports” is a property.

(Property imports)

%% Both arguments of “imports” are ontologies.

(Domain imports Ontology)

(Range imports Ontology)

<comment>for equivalentTo(X, Y), read X is an equivalent term to Y.

</comment>

</Property>

%% “equivalentTo” is a property.

(Property equivalentTo)

%% “equivalentTo” means that two terms denote the same object.

(<=> (equivalentTo ?x ?y) (= ?x ?y))

%% Note: “equivalentTo” is a subproperty of “subPropertyOf” only when the arguments are properties, and is a subproperty of “subClassOf” only when the arguments are classes.

(=> (equivalentTo ?p1 ?p2) (Property ?p1) (Property ?p2)

(subPropertyOf ?p1 ?p2))

(=> (equivalentTo ?c1 ?c2) (Class ?c1) (Class ?c2)

(subClassOf ?c1 ?c2))

</Ontology>

<!-- the subPropertyOf is for the benefit of agents that know RDFS

but don't know DAML. -->

</Property>

%% “subPropertyOf” is a property.

(Property subPropertyOf)

%% Both arguments of “subPropertyOf” are properties.

(Domain subPropertyOf Property)

(Range subPropertyOf Property)

%% If a subproperty hold for two arguments, the “super” property also holds for those two arguments.

(<=> (subPropertyOf ?p1 ?p2) (=> (holds ?p1 ?x ?y) (holds ?p2 ?x ?y)))

</Class>

%% A unary relation is a relation that always takes exactly one argument.

(<=> (UnaryRelation ?r)

(and (Relation ?r)

(forall @args (=> (holds ?r @args)

(= (length (listof @args)) 1)))))

%% “Class” is a unary relation, and classes are unary relations.

(UnaryRelation Class)

(=> (Class ?c) (UnaryRelation ?c))

</Class>

%% “Literal” is a class.

(Class Literal)

</Class>

%% A binary relation is a relation that always takes exactly two arguments.

(<=> (BinaryRelation ?r)

(and (Relation ?r)

(forall @args (=> (holds ?r @args)

(= (length (listof @args)) 2)))))

%% “Property” is a class, and properties are binary relations.

(Class Property)

(=> (Property ?p) (BinaryRelation ?p))

</Property>

%% “type” is a property.

(Property type)

% The second argument of “type” is a class.

(Range type Class)

</Property>

%% “value” is a property.

(Property value)

</Property>

%% “subClassOf” is a property.

(Property subClassOf)

%% The arguments of “subClassOf” are classes.

(Domain subClassOf Class)

(Range subClassOf Class)

%% Instances of a subclass are also instances of the superclass.

(=> (subClassOf ?csub ?csuper) (type ?x ?csub) (type ?x ?csuper)))

</Property>

%% “domain” is a property.

(Property domain)

%% The object in an RDF statement of the form “(object property resource)” must be an instance of the domain of property.

(=> (Property ?p) (domain ?p ?d) (holds ?p ?x ?y) (type ?x ?d))

</Property>

%% “range” is a property.

(Property range)

%% The resource in an RDF statement of the form “(object property resource)” must be an instance of the range of property.

(=> (Property ?p) (range ?p ?r) (holds ?p ?x ?y) (type ?y ?r))

</Property>

%% “label” is a property.

(Property label)

</Property>

%% “comment” is a property.

(Property comment)

</Property>

%% “seeAlso” is a property.

(Property seeAlso)

</Property>

%% “isDefinedBy” is a property.

(Property isDefinedBy)

<label>default</label>

<comment>default(X, Y) suggests that Y be considered a/the default

value for the X property. This can be considered

documentation (ala label, comment) but we don't specify

any logical impact.

</comment>

</Property>

%% “default” is a property.

(Property default)

%% The first argument of “default” is a property.

(domain default Property)

<!-- from RDF, left out:

Bag, Alt: why bother? note that we can't import

the syntax of these into the DAML namespace if we expect

RDF 1.0 parsers to grok.

predicate, subject, object, Statement: DAML audience doesn't need quoting.

-->

<!-- from RDFS, left out

Container: the motivation for this, to somehow denote that other

element names can be used with the <li> syntax, is busted.

ContainerMembershipProperty: without the <li> syntax, not much use for this.

ConstraintResource, ConstraintProperty: I don't grok these.

-->

</rdf:RDF>

[1] KIF note: Relational sentences in KIF have the form “ (<relation name> <argument>*)”.

[2] KIF notes: Names whose first character is ``?'' are variables. If no explicit quantifier is specified, variables are assumed to be universally quantified.

[3] KIF notes: “=>” means “implies”. “<=>” means “if and only if”.

[5] KIF notes: For an implication that has N arguments, where N is greater than 2, the first N-1 arguments are considered to be a conjunction that is the antecedent and the Nth argument is considered to be the consequent. I.e., “(=> arg₁ arg₂ … arg_N)” is equivalent to “(=> (and arg₁ arg₂ … arg_N-1) arg_N)”. “~=” means “not equal”. I.e., “(~= t1 t2)” is equivalent to “(not (= t1 t2))”. “=” means “denotes the same object in the domain of discourse”.

[6] KIF notes: Names whose first character is "@" are sequence variables that bind to a sequence of 0 or more objects. For example, the expression “(F @X)” binds to “(F 14 23)” and in general to any list whose first element is “F”. “listof” is a function in KIF which denotes the list those elements are the objects denoted by the function’s arguments.

[7] KIF note: “integer” and “negative” are KIF relations on numbers.

[8] KIF note: “holds” means “relation is true for”. One must use the form “(holds ?C ?I)” rather than “(?C ?I)” when the relation is a variable because KIF has a first-order logic syntax and therefore does not allow a variable in the first position of a relational sentence.

[9] KIF note: “length” is a KIF function that denotes the number of items in the list denoted by the argument of “length”.

[10] KIF note: “=<” is the KIF relation for “less than or equal”.

[11] KIF note: “>=” is the KIF relation for “greater than or equal”.