An Axiomatic Semantics for DAML-ONT

Richard Fikes

Deborah L McGuinness

Knowledge Systems Laboratory

Computer Science Department

Stanford University

November 13, 2000

An updated version of this document is available at http://www.ksl.stanford.edu/people/dlm/DAML-Ont-kif-axioms-001127.html

Introduction

This document specifies a formal 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 a logically equivalent translation of a DAML-ONT ontology. Our intent is to provide a precise, succinct, and formal description of the properties and classes in DAML-ONT (e.g., complementOf, intersectionOf, Nothing). The axioms provide that description by providing if-and-only-if definitions of some DAML-ONT properties and by specifying a set of restrictions on the possible interpretations of the remaining properties and on DAML-ONT classes. The axioms are written in ANSI Knowledge Interchange Format (KIF) (http://logic.stanford.edu/kif/kif.html), which is a proposed ANSI standard.

A logical theory in KIF that is logically equivalent to a DAML-ONT ontology can be produced as follows:

· Translate each declaration of a class C in the DAML-ONT ontology into a KIF sentence of the form “(Class C)”.

· Translate each declaration of a property P in the DAML-ONT ontology into a KIF sentence of the form “(Property P)”.

· Translate each RDF statement with predicate P, subject S, and object O into a KIF sentence of the form “(P S O)”.

· Include in the KIF theory all of the axioms in this document.

Since KIF has a model theoretic semantics and this document specifies how to translate a DAML-ONT ontology into an equivalent KIF logical theory, we have in effect specified a model theoretic semantics for DAML-ONT.

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”. Axioms have labels of the form “Axn”, where “n” is the axiom number.

We also include a set of simple theorems that are inferable from the axioms as additional commentary. Theorems have labels of the form “Thn”, where “n” is the theorem number.

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, and List.

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

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.

Ax1. (Class Thing)[2]

%% Every object is type Thing.

Ax2. (Thing ?x)[3]

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

</Class>

%% “Nothing” is a Class.

Ax3. (Class Nothing)

%% No object is type Nothing.

Ax4. (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.

Ax5. (Property disjointWith)

%% Saying that two objects are “disjointWith” is equivalent to saying that the two objects are classes, that the classes have no instances in common, and that at least one of the classes has an instance.

Ax6. (<=> (disjointWith ?c1 ?c2)

(Class ?c1)

(Class ?c2)

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

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

%% Note that the following can be inferred from the axioms regarding “disjointWith”, “domain”, and “range”:

Th1. (domain disjointWith Class)

Th2. (range disjointWith Class)

<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 “Class”.

Ax7. (Class Disjoint)

Ax7.

%% Saying that an object is “Disjoint” is equivalent to saying that the object is a list, that every item in the list is a class, and that the classes in the list are pairwise joint.

Ax8. (<=> (Disjoint ?l)

(and (List ?l)

(forall (?c) (=> (Item ?c ?l) (Class ?c)))

(forall (?c1 ?c2)

(=> (Item ?c1 ?l) (Item ?c2 ?l) (/= ?c1 ?c2)

(DisjointWith ?c1 ?c2)))))[5]

%% Note that the following can be inferred from the axioms regarding “Disjoint” and “subClassOf”:

Th3. (subClassOf Disjoint List)

Th3.

Th3.<Property ID="unionOf">

<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.

Ax9. (Property unionOf)

%% Saying that objects C1 and L are “unionOf” is equivalent to saying that C1 is a class, L is a list, every item in list L is a class, and the instances of class C1 are exactly the instances of all the classes in the list L.

Ax10. (<=> (unionOf ?c1 ?l)

(and (Class ?c1)

(List ?l)

(forall (?x) (=> (item ?x ?l) (Class ?x)))

(forall (?x) (<=> (type ?x ?c1)

(exists (?c2)

(and (item ?c2 ?l)

(type ?x ?c2)))))))[6]

%% Note that the following can be inferred from the axioms regarding “unionOf”, “domain”, and “range”:

Th4. (domain unionOf Class)

Th5. (range unionOf List)

<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.

Ax11. (Property disjointUnionOf)

%% Saying that objects C and L are “disjointUnionOf” is equivalent to saying that C is a class that is the union of the list L of classes and that the classes in list L are pairwise disjoint.

Ax12. (<=> (disjointUnionOf ?c ?l)

(and (unionOf ?c ?l) (Disjoint ?l)))

%% Note that the following can be inferred from the axioms regarding “disjointUnionOf”, “unionOf”, “domain”, and “range”:

Th6. (domain disjointUnionOf Class)

Th7. (range disjointUnionOf Disjoint)

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.

Ax13. (Property intersectionOf)

%% Saying that two objects C1 and L are “intersectionOf” is equivalent to saying that C1 is a class, L is a list, all of the items in list L are classes, and the instances of class C1 are exactly those objects that are instances of all the classes in list L.

Ax14. (<=> (intersectionOf ?c1 ?l)

(and (Class ?c1)

(List ?l)

(forall (?x) (=> (item ?x ?l) (Class ?x)))

(forall (?x) (<=> (type ?x ?c1)

(forall (?c2)

(=> (item ?c2 ?l)

(type ?x ?c2 ))))))

%% Note that the following can be inferred from the axioms regarding “intersectionOf”, “domain”, and “range”:

Th8. (domain intersectionOf Class)

Th9. (range intersectionOf List)

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.

Ax15. (Property complementOf)

%% Saying that objects C1 and C2 are “complementOf” is equivalent to saying that C1 and C2 are disjoint classes and all objects are instances of either C1 or C2.

Ax16. (<=> (complementOf ?c1 ?c2)

(and (disjointWith ?c1 ?c2)

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

%% Note that the following can be inferred from the axioms regarding “complementOf”, “disjointWith”, “domain”, “range”, “Thing”, and “Nothing”:

Th10. (domain complementOf Class)

Th11. (range complementOf Class)

Th12. (complementOf Thing Nothing)

</Class>

%%”List” is a class.

Ax17. (Class List)

%% A list is a sequence.

Ax18. (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.

Ax19. (Property oneOf)

%% Saying that objects C and L are “oneOf” is equivalent to saying that C is a class, L is a list, and the instances of class C are exactly the items in list L.

Ax20. (<=> (oneOf ?c ?l)

(and (Class ?c)

(List ?l)

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

%% Note that the following can be inferred from the axioms regarding “oneOf”, “domain”, and “range”:

Th13. (domain oneOf Class))

Th14. (range oneOf List)

</Class>

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

Ax21. (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.

Ax22. (Property asClass)

%% Both arguments of “asClass” are classes.

(domain asClass Class)

(range asClass Class)

%% Saying that objects C1 and C2 are “asClass” is equivalent to saying that C1 and C2 denote the same class.

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

(and (Class ?c1) (Class ?c2) (= ?c1 ?c2)))

%% Note that the following can be inferred from the axioms regarding “asClass”, “domain”, and “range”:

Th15. (domain asClass Class)

Th16. (range asClass Class)

</Property>

%% “first” is a property.

Ax24. (Property first)

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

(domain first List)

%% Saying that objects L and X are “first” is equivalent to saying that L is a list whose first item is X.

Ax25. (<=> (first ?l ?x)

(and (List ?l)

(exists (?r) (= ?l (cons ?x ?r))))[7]

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

</Property>

%% “rest” is a property.

Ax26. (Property rest)

%% Saying that objects L and R are “rest” is equivalent to saying that L is a list, R is a list, and L has the same items in the same order as list R with one additional object as its first item.

Ax27. (<=> (rest ?l ?r)

(and (List ?l)

(List ?r)

(exists (?x) (= ?l (cons ?x ?r)))))

%% Note that the following can be inferred from the axioms regarding “oneOf”, “domain”, and “range”:

Th17. (domain rest List))

Th18. (range rest List)

<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.

Ax28. (Property item)

%% Saying that objects L and X are “item” is equivalent to saying that L is a list and either X is the first item in list L or there is a list R that is the rest of list L and X is an item in the list R.

Ax29. (<=> (item ?l ?x)

(and (List ?l)

(or (first ?l ?x)

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

%% Note that the following can be inferred from the axioms regarding “item”, and “domain”:

Th19. (domain item List))

<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.

Ax30. (Property cardinality)

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

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

(or (= ?l (listof))

(exists (?x) (= ?l (listof ?x)))

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

(no-repeats-list (rest ?l)))))[8]

%% 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.

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

(and (Property ?p)

(no-repeats-list ?ys)

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

%% Saying that objects P and N are “cardinality” is equivalent to saying that P is a property and for all objects X, the length of the values list of P and X is equal to N.

Ax33. (<=> (cardinality ?p ?n)

(and (Property ?p)

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

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

%% Note that the following can be inferred from the axioms regarding “cardinality”, “domain”, “range”, and “length”:

Th20. (domain cardinality Property)

Th21. (range cardinality Integer)

Th22. (=> (cardinality ?p ?n) (not (negative ?n)))[11]

<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.

Ax34. (Property maxCardinality)

%% Saying that objects P and N are “maxCardinality” is equivalent to saying that P is a property and for all objects X, the length of the values list of P and X is less than or equal to N.

Ax35. (<=> (maxCardinality ?p ?n)

(and (Property ?p)

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

%% Note that the following can be inferred from the axioms regarding “cardinality”, “domain”, “range”, and “length”:

Th23. (domain maxCardinality Property)

Th24. (range maxCardinality Integer)

Th25. (=> (maxCardinality ?p ?n) (not (negative ?n)))

<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.

Ax36. (Property minCardinality)

%% Saying that objects P and N are “minCardinality” is equivalent to saying that P is a property and for all objects X, the length of the values list of P and X is greater than or equal to N.

Ax37. (<=> (minCardinality ?p ?n)

(and (Property ?p)

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

%% Note that the following can be inferred from the axioms regarding “minCardinality”, “domain”, “range”, and “length”:

Th26. (domain minCardinality Property)

Th27. (range minCardinality Integer)

Th28. (=> (minCardinality ?p ?n) (not (negative ?n)))

<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.

Ax38. (Property inverseOf)

%% Both arguments of “inverseOf” are properties.

(domain inverseOf Property)

(range inverseOf Property)

%% Saying that objects P1 and P2 are “inverseOf” is equivalent to saying that P1 is a property, P2 is a property, and that P1 and P2 hold for the same objects but with the arguments in reverse order.

Ax39. (<=> (inverseOf ?p1 ?p2)

(and (Property ?p1)

(Property ?p2)

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

(holds ?p2 ?x2 ?x1)))))

%% Note that the following can be inferred from the axioms regarding “inverseOf”, “domain”, and “range”:

Th29. (domain inverseOf Property)

Th30. (range inverseOf Property)

%%”TransitiveProperty” is a class.

Ax40. (Class TransitiveProperty)

%% Saying that an object P is a “TransitiveProperty” is equivalent to saying that P is a property and that P is a transitive relation.

Ax41. (<=> (TransitiveProperty ?p)

(and (Property ?p)

(forall (?x ?y ?z)

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

(holds ?p ?x ?z)))))

%% Note that the following can be inferred from the axioms regarding “TransitiveProperty” and “subClassOf”:

Th31. (subClassOf TransitiveProperty Property)

<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>

%%”UniqueProperty” is a class.

Ax42. (Class UniqueProperty)

%% Saying that object P is a “UniqueProperty” is equivalent to saying that P is a property and P holds for at most one second argument for each first argument.

Ax43. (<=> (UniqueProperty ?p)

(and (Property ?p)

(forall (?x ?y ?z)

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

(= ?y ?z)))))

%% Note that the following can be inferred from the axioms regarding “UniqueProperty” and “subClassOf”:

Th32. (subClassOf UniqueProperty Property)

<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>

%% Saying that an object P is an “UnambiguousProperty” is equivalent to saying that P is a property and P holds for at most one first argument for each second argument.

Ax44. (<=> (UnambiguousProperty ?p)

(and (Property ?p)

(forall (?x ?y ?v)

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

(= ?x ?y)))))

%% Note that the following can be inferred from the axioms regarding “UnambiguousProperty” and “subClassOf”:

Th33. (subClassOf UnambiguousProperty Property)

%% “Restriction” is a Class.

Ax45. (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.

Ax46. (Property restrictedBy)

%% The first argument of restrictedBy is a class.

Ax47. (domain restrictedBy Class)

%% The second argument of restrictedBy is a restriction.

Ax48. (range restrictedBy Restriction)

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

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

</Property>

%% “onProperty” is a property.

Ax49. (Property onProperty)

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

Ax50. (=> (onProperty ?rq ?p)

(or (Restriction ?rq) (Qualification ?rq)))

%% The second argument of onProperty is a property.

Ax51. (range onProperty Property)

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

</Property>

%% “toValue” is a property.

Ax52. (Property toValue)

%% The first argument of toValue is a restriction.

Ax53. (domain toValue Restriction)

%% Note: We are assuming the range restriction given in the DAML-ONT specification 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 constrains each instance of the class to have the second argument of “toValue” as a value of that property.

Ax54. (=> (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.

Ax55. (Property toClass)

%% The first argument of toClass is a restriction.

Ax56. (domain toClass Restriction)

%% The second argument of toClass is a class.

Ax57. (range toClass Class)

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

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

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

%% “Qualification” is a Class.

Ax59. (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.

Ax60. (Property qualifiedBy)

%% The first argument of qualifiedBy is a class.

Ax61. (domain qualifiedBy Class)

%% The second argument of qualifiedBy is a qualification.

Ax62. (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.

Ax63. (Property hasValue)

%% The first argument of hasValue is a qualification.

Ax64. (domain hasValue Qualification)

%% The second argument of hasValue is a class.

Ax65. (range hasValue Class)

%% A “hasValue” qualification on a property on a class constrains each instance of the class to have a value for that property that is type the class that is the second argument of “hasValue”.

Ax66. (=> (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 .

%% Note that the following can be inferred from the axioms regarding “qualifiedBy”, “onProperty”, “hasValue” and “minCardinality”:

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

(minCardinality ?p 1))

<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.

Ax67. (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.

Ax68. (Property versionInfo)

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

Ax69. (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.

Ax70. (Property imports)

%% Both arguments of “imports” are ontologies.

Ax71. (domain imports Ontology)

Ax72. (range imports Ontology)

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

</comment>

</Property>

%% “equivalentTo” is a property.

Ax73. (Property equivalentTo)

%% Saying that objects X and Y are “equivalentTo” is equivalent to saying that X and Y denote the same object (i.e., that they are equal).

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

</Ontology>

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

but don't know DAML. -->

</Property>

%% “subPropertyOf” is a property.

Ax75. (Property subPropertyOf)

%% Saying that objects P1 and P2 are “subPropertyOf” is equivalent to saying that P1 is a property, P2 is a property, and that if P1 holds for some objects X and Y, then P2 also holds for X and Y.

Ax76. (<=> (subPropertyOf ?p1 ?p2)

(and (Property ?p1)

(Property ?p2)

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

%% Note that the following can be inferred from the axioms regarding “subPropertyOf”, “domain”, “range” and “equivalentTo”:

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

(subPropertyOf ?p1 ?p2))

Th36. (domain subPropertyOf Property)

Th37. (range subPropertyOf Property)

</Class>

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

Ax77. (<=> (UnaryRelation ?r)

(and (Relation ?r)

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

(= (length (listof @args)) 1)))))[14]

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

Ax78. (UnaryRelation Class)

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

</Class>

%% “Literal” is a class.

Ax80. (Class Literal)

</Class>

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

Ax81. (<=> (BinaryRelation ?r)

(and (Relation ?r)

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

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

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

Ax82. (Class Property)

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

</Property>

%% “type” is a property.

Ax84. (Property type)

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

Ax85. (range type Class)

</Property>

%% “value” is a property.

Ax86. (Property value)

</Property>

%% “subClassOf” is a property.

Ax87. (Property subClassOf)

%% The arguments of “subClassOf” are classes.

Ax88. (domain subClassOf Class)

Ax89. (range subClassOf Class)

Ax89.

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

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

(type ?x ?csuper)))

%% Note that the following can be inferred from the axioms regarding “subClassOf” and “equivalentTo”:

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

(subClassOf ?c1 ?c2))

</Property>

%% “domain” is a property.

Ax91. (Property domain)

%% Saying that objects P and D are “domain” implies that P is a property, D is a class, and for any objects X and Y that are “P”, X must be type D.

Ax92. (=> (domain ?p ?d)

(and (Property ?p)

(Class ?d)

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

%% Note that the following can be inferred from the axioms regarding “domain” and “range”:

Th39. (domain domain Property)

Th40. (range domain Class)

</Property>

%% “range” is a property.

Ax93. (Property range)

%% Saying that object P and R are “range” implies that P is a property, R is a class, and for any objects X and Y that are “P”, Y must be type R.

Ax94. (=> (range ?p ?r)

(and (Property ?p)

(Class ?r)

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

%% Note that the following can be inferred from the axioms regarding “domain” and “range”:

Th41. (domain range Property)

Th42. (range range Class)

</Property>

%% “label” is a property.

Ax95. (Property label)

</Property>

%% “comment” is a property.

Ax96. (Property comment)

</Property>

%% “seeAlso” is a property.

Ax97. (Property seeAlso)

</Property>

%% “isDefinedBy” is a property.

Ax98. (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.

Ax99. (Property default)

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

Ax100.(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] The authors would like to thank Pat Hayes for his generous help in debugging earlier versions of this document.

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

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

[4] KIF note: “<=>” means “if and only if”.

[5] KIF notes: “=>” means “implies”. 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”.

[7] KIF note: “cons” is a KIF function that takes an object and a list as arguments and whose value is the list produced by adding the object to the beginning of the list so that the object is the first item on the list that is the function’s value.

[8] KIF notes: “(listof)” is a term that denotes an empty list. “(listof x)” is a term that denotes the list of length 1 whose first (and only) item is x.

[9] 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.

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

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

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

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

[14] KIF note: 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”.