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 [email protected] 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>

<imports resource="http://www.w3.org/2000/01/rdf-schema"/>

</rdf:Description>

<!-- Terms for building classes from other classes. -->

<Class ID="Thing">

<label>Thing</label>

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

</Class>

%% “Thing” is a Class.(Class Thing)

%% Every object is an instance of Thing.

(Thing ?x)

<Class ID="Nothing">

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

<complementOf resource="#Thing"/>

</Class>

%% “Nothing” is a Class.(Class Nothing)

%% No object is an instance of Nothing.(not (Nothing ?x))

<Property ID="disjointWith">

<label>disjointWith</label>

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

in common.

</comment>

<domain resource="#Class"/>

<range resource="#Class"/>

</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)))))<Class ID="Disjoint"> <label>Disjoint</label>

<subClassOf resource="#List"/>

<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)) %% The items in a “Disjoint” list are pairwise disjoint.(=> (Disjoint ?l)

(Item ?c1 ?l)

(Item ?c2 ?l)

(~= ?c1 ?c2)

(DisjointWith ?c1 ?c2))<Property ID="unionOf">

<label>unionOf</label>

<comment>

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>

<domain resource="#Class"/>

<range resource="#List"/>

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

<Property ID="disjointUnionOf">

<label>disjointUnionOf</label>

<domain resource="#Class"/>

<range resource="#List"/>

<comment>

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

<Property ID="intersectionOf">

<comment>

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>

<domain resource="#Class"/>

<range resource="#List"/>

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

<Property ID="complementOf">

<comment>

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>

<domain resource="#Class"/>

<range resource="#Class"/>

</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.<!-- List terminology. -->

<Class ID="List">

<subClassOf resource="http://www.w3.org/1999/02/22-rdf-syntax-ns#Seq"/>

</Class>

%%”List” is a class.

(Class List)

%% A list is a sequence.

(subClassOf List Seq)

<Property ID="oneOf">

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

<domain resource="#Class"/>

<range resource="#List"/>

</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 ID="Empty">

<asClass resource="#Nothing"/>

</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 ID="first">

<domain resource="#List"/>

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

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

<Property ID="rest">

<domain resource="#List"/>

<range resource="#List"/>

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

<Property ID="item">

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

<domain resource="#List"/>

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

<!-- facets of properties. -->

<Property ID="cardinality">

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

<domain resource="#Property"/>

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

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

<Property ID="maxCardinality">

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

<domain resource="#Property"/>

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

<Property ID="minCardinality">

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

<domain resource="#Property"/>

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

<Property ID="inverseOf">

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

<domain resource="#Property"/>

<range resource="#Property"/>

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

<Class ID="TransitiveProperty"/>

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

<Class ID="UniqueProperty">

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

<subClassOf resource="#Property"/>

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

<Class ID="UnambiguousProperty">

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

<subClassOf resource="#Property"/>

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

<!-- Terms for restricting properties of things in classes. -->

<Class ID="Restriction"/>

%% “Restriction” is a Class.(Class Restriction)

<Property ID="restrictedBy">

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

<domain resource="#Class"/>

<range resource="#Restriction"/>

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

<Property ID="onProperty">

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

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

<domain resource="#Restriction"/>

<domain resource="#Qualification"/>

<range resource="#Property"/>

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

<Property ID="toValue">

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

<domain resource="#Restriction"/>

<range resource="#Class"/>

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

<Property ID="toClass">

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

<domain resource="#Restriction"/>

<range resource="#Class"/>

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

<Class ID="Qualification"/>

%% “Qualification” is a Class.(Class Qualification)

<Property ID="qualifiedBy">

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

<domain resource="#Class"/>

<range resource="#Qualification"/>

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

<Property ID="hasValue">

<label>hasValue</label>

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

qualification to C.</comment>

<domain resource="#Qualification"/>

<range resource="#Class"/>

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

<!-- A class for ontologies themselves... -->

<Class ID="Ontology">

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

<Property ID="versionInfo">

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

<!-- Importing, i.e. assertion by reference -->

<Property ID="imports">

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

<!-- Renaming -->

<Property ID="equivalentTo"> <!-- equals? equiv? renames? -->

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

</comment>

<!--@@RDF specs prohibits cycles, but I don't buy it. -->

<subPropertyOf resource="#subPropertyOf"/>

<subPropertyOf resource="#subClassOf"/>

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

<!-- Importing terms from RDF/RDFS -->

<!-- first, assert the contents of the RDF schema by reference -->

<Ontology about="">

<imports resource="http://www.w3.org/2000/01/rdf-schema"/>

</Ontology>

<Property ID="subPropertyOf">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#subPropertyOf"/>

<subPropertyOf resource="http://www.w3.org/2000/01/rdf-schema#subPropertyOf"/>

<!-- 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 ID="Class">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#Class"/>

</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 ID="Literal">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>

</Class>

%% “Literal” is a class.

(Class Literal)

<Class ID="Property">

<equivalentTo resource="http://www.w3.org/1999/02/22-rdf-syntax-ns#Property"/>

</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 ID="type">

<equivalentTo resource="http://www.w3.org/1999/02/22-rdf-syntax-ns#type"/>

</Property>

%% “type” is a property.

(Property type)

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

(Range type Class)

<Property ID="value">

<equivalentTo resource="http://www.w3.org/1999/02/22-rdf-syntax-ns#value"/>

</Property>

%% “value” is a property.

(Property value)

<Property ID="subClassOf">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#subClassOf"/>

</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 ID="domain">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#domain"/>

</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 ID="range">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#range"/>

</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 ID="label">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#label"/>

</Property>

%% “label” is a property.

(Property label)

<Property ID="comment">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#comment"/>

</Property>

%% “comment” is a property.

(Property comment)

<Property ID="seeAlso">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#seeAlso"/>

</Property>

%% “seeAlso” is a property.

(Property seeAlso)

<Property ID="isDefinedBy">

<equivalentTo resource="http://www.w3.org/2000/01/rdf-schema#isDefinedBy"/>

<subPropertyOf resource="#seeAlso"/>

</Property>

%% “isDefinedBy” is a property.

(Property isDefinedBy)

<Property ID="default">

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

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

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