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
$Id: daml-ont.daml,v 1.2 2000/10/11 06:30:02 connolly Exp
$The most general class in DAML.
%% "Thing" is a Class.
(Class Thing)
%% Every object is an instance of Thing.
(Thing ?x)
the class with no things in it.
%% "Nothing" is a Class.
(Class Nothing)
%% No object is an instance of Nothing.
(not (Nothing ?x))
for disjointWith(X, Y) read: X and Y have no members
in common.
%% "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)))))
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).
%% A "Disjoint" is a "List".
(subClassOf Disjoint List)
%% All items in a "Disjoint" list are classes.
(=> (Disjoint ?l) (Item ?c ?l) (Class ?c))
%% The items in a "Disjoint" list are pairwise disjoint.
(=> (Disjoint ?l)
(Item ?c1 ?l)
(Item ?c2 ?l)
(~= ?c1 ?c2)
(DisjointWith ?c1 ?c2))
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
%% "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)))))
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
%% "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
%% "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
%% "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.
%%"List" is a class.
(Class List)
%% A list is a sequence.
(subClassOf List Seq)
for oneOf(C, L) read everything in C is one of the
things in L;
This lets us define classes by enumerating the members.
%% "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)))
%% "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))
%% "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))))
%%Note: DAML-ONT seems to need an equivalent of KIF's "listof" as part
of the language.
%% "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)))))
for item(L, I) read: I is an item in L; either first(L, I)
or item(R, I) where rest(L, R).
%% "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)))))
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).
%% "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))))
%% 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)))))
%% 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)))
%%Note: DAML-ONT seems to need an equivalent of KIF's "length" function
as part of the language.
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).
%% "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)))
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).
%% "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)))
for inverseOf(R, S) read: R is the inverse of S; i.e.
if R(x, y) then S(y, x) and vice versa.
%% "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))))
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.
%% 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))
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.
%% 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)
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).
%% "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)
for onProperty(R, P), read:
R is a restriction/qualification on P.
%% "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)
for toValue(R, V), read: R is a restriction to V.
%% "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)))
for toClass(R, C), read: R is a restriction to C.
%% "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)
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).
%% "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)
for hasValue(Q, C), read: Q is a hasValue
qualification to C.
%% "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 .
An Ontology is a document that describes
a vocabulary of terms for communication between
(human and) automated agents.
%% An ontology is a class.
(Class Ontology)
generally, a string giving information about this
version; e.g. RCS/CVS keywords
%% "versionInfo" is a property.
(Property versionInfo)
%% The first argument of "versionInfo" is an ontology.
(Domain versionInfo Ontology)
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".
%% "imports" is a property.
(Property imports)
%% Both arguments of "imports" are ontologies.
(Domain imports Ontology)
(Range imports Ontology)
for equivalentTo(X, Y), read X is an equivalent term to Y.
%% "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))
%% "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)))
%% 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))
%% "Literal" is a class.
(Class Literal)
%% 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))
%% "type" is a property.
(Property type)
% The second argument of "type" is a class.
(Range type Class)
%% "value" is a property.
(Property value)
%% "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)))
%% "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))
%% "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))
%% "label" is a property.
(Property label)
%% "comment" is a property.
(Property comment)
%% "seeAlso" is a property.
(Property seeAlso)
%% "isDefinedBy" is a property.
(Property isDefinedBy)
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.
%% "default" is a property.
(Property default)
%% The first argument of "default" is a property.
(domain default Property)
KIF note: Relational sentences in KIF have the form " (*)".
KIF notes: Names whose first character is ``?'' are variables. If no explicit quantifier is specified, variables
are assumed to be universally quantified.
KIF notes: "=>" means "implies". "<=>" means "if and only if".
KIF note: "=>" means "implies".
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., "(=> arg1 arg2 … argN)" is equivalent to "(=> (and arg1 arg2 … argN-1) argN)". "~=" means
"not equal". I.e., "(~= t1 t2)" is equivalent to "(not (= t1 t2))". "=" means "denotes the same object in the
domain of discourse".
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.
KIF note: "integer" and "negative" are KIF relations on numbers.
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.
KIF note: "length" is a KIF function that denotes the number of items in the list denoted by the argument
of "length".
KIF note: "=<" is the KIF relation for "less than or equal".
KIF note: ">=" is the KIF relation for "greater than or equal".