An Axiomatic Semantics for RDF, RDF Schema, and
DAML-ONT
Richard Fikes
Deborah L McGuinness
Knowledge Systems Laboratory
Computer Science Department
Stanford University
November 27, 2000
Note: There is an updated version of this paper. Please use that version. It is
available at: www.ksl.stanford.edu/people/dlm/DAML-Ont-kif-axioms-001129.txt
1. Introduction
This document provides an axiomatization for the Resource Description Framework (RDF),
RDF Schema, and DAML-ONT by specifying a mapping of a set of descriptions in any one of
these languages into a logical theory expressed in first-order predicate calculus. The basic claim
of this paper is that the logical theory produced by the mapping specified herein of a set of such
descriptions is logically equivalent to the intended meaning of that set of descriptions.
The mapping consists of a simple rule for translating RDF (http://www.w3.org/TR/REC-rdf-
syntax/) statements into first-order relational sentences and a set of first-order logic axioms that
restrict the allowable interpretations of the non-logical symbols (i.e., relations, functions, and
constants) in each language. Since RDF Schema (http://www.w3.org/TR/rdf-schema/) and
DAML-ONT (http://www.daml.org/2000/10/daml-ont.html) are both vocabularies of non-
logical symbols added to RDF, the translation of RDF statements is sufficient for translating
RDF Schema and DAML-ONT as well.
The axioms are written in ANSI Knowledge Interchange Format (KIF)
(http://logic.stanford.edu/kif/kif.html), which is a proposed ANSI standard. The axioms use
standard first-order logic constructs plus KIF-specific relations and functions dealing with lists.
Lists as objects in the domain of discourse are needed in order to axiomatize RDF containers
and the DAML-ONT properties dealing with cardinality.
The mapping of each of these languages into first-order logic is as follows: A logical theory in
KIF that is logically equivalent to a set of RDF, RDF Schema, or DAML-ONT descriptions
can be produced as follows:
? Translate each RDF statement with predicate P, subject S, and object O into a KIF
sentence of the form "(PropertyValue P S O)".
? Include in the KIF theory the axioms in this document associated with the source language
(RDF, RDF Schema, or DAML-ONT).
Note that it is not necessary to specify a translation for every construct in RDF since any set of
RDF descriptions can be translated into an equivalent set of RDF statements. Thus, the one
translation rule above suffices to translate all of RDF and of the other two languages as well.
This axiomatization is designed to place minimal constraints on the interpretation of the non-
logical symbols in the resulting logical theory. In particular, the axioms do not require that
classes be considered to be sets or to be unary relations, nor do they require that properties be
considered to be mappings or binary relations. Such constraints could be added to the resulting
logical theory if desired, but they are not needed to express the intended meaning of the RDF,
RDF Schema, or DAML-ONT descriptions being translated.
Comments are welcomed posted to the www-rdf-logic@w3.org distribution list.
2. KIF Supporting Definitions
We define the following KIF relations for use in representing RDF, RDF Schema, and DAML-
ONT descriptions in KIF.
2.1. PropertyValue
"PropertyValue" is a ternary relation such that each RDF statement with any predicate P, any
subject S, and any object O is translated into the KIF relational sentence "(PropertyValue P S
O)".
2.2. Type
"Type" is a binary relation that provides a shorthand notation for RDF statements whose
predicate is the property "type".
%% Saying that relation "Type" holds for objects S and O is equivalent
to saying that relation "PropertyValue" holds for objects "type", S, and
O.
Ax1. (<=> (Type ?s ?o) (PropertyValue type ?s ?o))
2.3. No Repeats List
This relation is used in the axiomatization of properties "cardinality", "minCardinality", and
"maxCardinality".
%% A "no-repeats-list" is a list for which no item occurs more than
once.
Ax2. (<=> (no-repeats-list ?l)
(or (= ?l nil)
(exists (?x) (= ?l (listof ?x)))
(and (not (item (rest ?l) (first ?l)))
(no-repeats-list (rest ?l)))))
3. RDF
As stated in the introduction, each RDF statement with predicate P, subject S, and object O is
translated into a KIF sentence of the form "(PropertyValue P S O)".
3.1. Classes
This section axiomatizes the classes that are included in RDF and defines one additional class
(i.e., FunctionalProperty) that is useful in axiomatizing other classes and properties.
3.1.1. Resource
All things being described by RDF expressions are called resources.
%% "Resource" is a class.
Ax3. (Type Resource Class)
3.1.2. Property
%% "Property" is a subclass of "Resource".
Ax4. (Type Property Class)
Ax5. (=> (Type ?p Property) (Type ?p Resource))
3.1.3. Class
%% "Class" is a subclass of "Resource" that is disjoint from "Property".
Ax6. (Type Class Class)
Ax7. (=> (Type ?c Class) (Type ?c Resource))
Ax8. (not (and (Type ?x Property) (Type ?x Class)))
3.1.4. FunctionalProperty
The class "FunctionalProperty" is not in RDF or RDF Schema. We define
"FunctionalProperty" only for convenience in axiomatizing other classes and properties.
%% "FunctionalProperty" is a subclass of "Property".
Ax9. (Type FunctionalProperty Class)
Ax10. (=> (Type ?a FunctionalProperty) (Type ?a Property))
%% A FunctionalProperty is functional in its object.
Ax11. (=> (and (PropertyValue ?a ?s ?o1)
(PropertyValue ?a ?s ?o2)
(Type ?a FunctionalProperty))
(= ?o1 ?o2))
3.1.5. Literal
%% "Literal" is a class.
Ax12. (Type Literal Class)
3.1.6. Statement
%% "Statement" is a subclass of "Resource".
Ax13. (Type Statement Class)
Ax14. (=> (Type ?s Statement) (Type ?s Resource))
%% Every statement has a predicate, a subject, and an object.
Ax15. (=> (Statement ?st)
(exists (?p ?s ?o)
(and (Predicate ?st ?p)
(Subject ?st ?r)
(Object ?st ?o))))
3.1.7. Container
%% "Container" is a subclass of "Resource".
Ax16. (Type Container Class)
Ax17. (=> (Type ?c Container) (Type ?c Resource))
%% A container is represented as a list.
Ax18. (=> (Type ?c Container) (List ?c))
%% A container is either a bag, a sequence, or an alternative.
Ax19. (=> (Type ?c Container)
(or (Type ?c Bag)
(Type ?c Seq)
(Type ?c Alt)))
3.1.7.1. Bag
%% A bag is a container.
Ax20. (Type Bag Class)
Ax21. (=> (Type ?b Bag) (Type ?b Container))
3.1.7.2. Seq
%% A sequence is a container.
Ax22. (Type Seq Class)
Ax23. (=> (Type ?s Seq) (Type ?s Container))
%% Bags and sequences are disjoint.
Ax24. (not (and (Type ?x Bag) (Type ?x Seq)))
3.1.7.3. Alt
%% An alternative is a container.
Ax25. (Type Alt Class)
Ax26. (=> (Type ?a Alt) (Type ?a Container))
3.1.7.4. ContainerMembershipProperty
%% A container membership property is a property.
Ax27. (Type ContainerMembershipProperty Class)
Ax28. (=> (Type ?c ContainerMembershipProperty) (Type ?c Property))
3.2. Properties
This section axiomatizes the properties that are included in RDF.
3.2.1. type
"type" is used to indicate that a resource is a member of a class.
%% "type" is a property.
Ax29. (Type type Property)
%% The first argument of "Type" is a resource and the second argument of
"Type" is a class.
Ax30. (=> (Type ?r ?c) (and (Type ?r Resource) (Type ?c Class)))
3.2.2. subject
%% "Subject" is a FunctionalProperty of a statement whose value is a
resource.
Ax31. (Type Subject FunctionalProperty)
Ax32. (=> (PropertyValue Subject ?st ?sb)
(and (Type ?st Statement) (Type ?sb Resource)))
3.2.3. predicate
%% "Predicate" is a FunctionalProperty of a statement whose value is a
property.
Ax33. (FunctionalProperty Predicate)
Ax34. (=> (PropertyValue Predicate ?st ?p)
(and (Type ?st Statement) (Type ?p Property)))
3.2.4. object
%% "Object" is a functional property of a statement whose value is
either a resource or a literal.
Ax35. (FunctionalProperty Object)
Ax36. (=> (PropertyValue Object ?st ?o)
(and (Type ?st Statement)
(or (Type ?o Resource) (Type ?o Literal))))
3.2.5. value
%% "value" is a property that maps a resource to a resource or literal.
Ax37. (Type value Property)
Ax38. (=> (PropertyValue value ?sv ?v)
(and (Type ?sv Resource)
(or (Type ?v Resource) (Type ?v Literal))))
3.2.6. _1, _2, _3, …
%% For each positive integer N, "_N" is a functional property of a
collection whose value is the Nth element of that collection.
Ax39. (FunctionalProperty _1)
Ax40. (=> (PropertyValue _1 ?c ?o) (Type Collection ?c))
and similarly for _2, _3, etc.
4. RDF Schema
RDF Schema is a collection of classes and properties that is added to RDF. Statements in
RDF Schema are RDF statements.
4.1. Classes
This section axiomatizes the classes that are added to RDF in RDF Schema.
4.1.1. ConstraintResource
"ConstraintResource" is a class of RDF schema constructs involved in the expression of
constraints.
%% Constraint resources are resources.
Ax41. (subClassOf ConstraintResource Resource)
4.1.2. ConstraintProperty
%% Constraint properties are those constraint resources that are also
properties.
Ax42. (<=> (Type ?cp ConstraintProperty)
(and (Type ?cp ConstraintResource)
(Type ?cp Property)))
4.2. Properties
This section axiomatizes the properties that are added to RDF in RDF Schema.
4.2.1. subClassOf
%% "subClassOf" is a property.
Ax43. (Type subClassOf Property)
%% The arguments of subClassOf are classes, and instances of a subclass
are also instances of the superclass.
Ax44. (=> (PropertyValue subClassOf ?csub ?csuper)
(and (Type ?csub Class)
(Type ?csuper Class)
(\= ?csub ?csuper)
(forall (?x) (=> (Type ?csub ?x) (Type ?csuper ?x)))))
4.2.2. subPropertyOf
%% "subPropertyOf" is a property.
Ax45. (Type subPropertyOf Property)
%% If a subProperty has a value V for an object O, then the
superproperty also has value V for object O is.
Ax46. (=> (PropertyValue subPropertyOf ?subP ?superP)
(and (Type ?subP Property)
(Type ?superP Property)
(forall (?o ?v) (=> (PropertyValue ?subP ?o ?v)
(PropertyValue ?superP ?o ?v)))))
4.2.3. seeAlso
%% "seeAlso" is a property whose arguments are resources.
Ax47. (Type seeAlso Property)
Ax48. (PropertyValue domain seeAlso Resource)
Ax49. (PropertyValue range seeAlso Resource)
4.2.4. isDefinedBy
%% "isDefinedBy" is a subproperty of "seeAlso".
Ax50. (PropertyValue subProperty isDefinedBy seeAlso)
4.2.5. comment
%% "comment" is a property whose value is a literal.
Ax51. (Type comment Property)
Ax52. (=> (PropertyValue comment ?s ?l) (Type ?l Literal))
4.2.6. label
%% "label" is a property whose value is a literal.
Ax53. (Type label Property)
Ax54. (=> (PropertyValue label ?s ?l) (Type ?l Literal))
4.3. Constraint Properties
%% Constraint properties are properties.
Ax55. (=> (Type ?x ConstraintProperty) (Type ?x Property))
4.3.1. range
%% "range" is a constraint property.
Ax56. (Type range ConstraintProperty)
%% Saying that object P and R are "range" is equivalent to saying that P
is a property, R is a class, and if an object Y is the value of P for a
subject X, then Y is an instance of R.
Ax57. (<=> (PropertyValue range ?p ?r)
(and (Type ?p Property)
(Type ?r Class)
(forall (?x ?y)
(=> (PropertyValue ?p ?x ?y)
(Type ?y ?r)))))
%% A property can have at most one range.
Ax58. (=> (and (PropertyValue range ?p ?r1)
(PropertyValue range ?p ?r2))
(= ?r1 ?r2))
%% Note that the following can be inferred from the axioms regarding
"domain" and "range":
Th1. (PropertyValue domain range Property)
Th2. (PropertyValue range range Class)
4.3.2. domain
%% "domain" is a constraint property.
Ax59. (Type domain ConstraintProperty)
%% Saying that objects P and D are "domain" is equivalent to saying that
P is a property, D is a class, and if an object Y is the value of P for
a subject X, then X must is an instance of D.
Ax60. (<=> (PropertyValue domain ?p ?d)
(and (Type ?p Property)
(Type ?d Class)
(forall (?x ?y)
(=> (PropertyValue ?p ?x ?y)
(Type ?x ?d)))))
%% Note that the following can be inferred from the axioms regarding
"domain" and "range":
Th3. (PropertyValue domain domain Property)
Th4. (PropertyValue range domain Class)
5. DAML-ONT
DAML-ONT is a collection of classes and properties that is added to RDF and RDF-Schema.
Statements in DAML-ONT are RDF statements.
5.1. Classes
This section axiomatizes the classes that are added to RDF and RDF Schema.
5.1.1. Thing
%% "Thing" is a Class.
Ax61. (Type Thing Class)
%% Every object is type Thing.
Ax62. (Type ?x Thing)
5.1.2. Nothing
%% "Nothing" is a Class.
Ax63. (Type Nothing Class)
%% No object is type Nothing.
Ax64. (not (Type ?x Nothing))
5.1.3. Disjoint
%% A "Disjoint" is a "Class".
Ax65. (Type Disjoint Class)
%% 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.
Ax66. (<=> (Type ?l Disjoint)
(and (Type ?l List)
(forall (?c) (=> (PropertyValue Item ?c ?l)
(Type ?c Class)))
(forall (?c1 ?c2)
(=> (and (PropertyValue item ?c1 ?l)
(PropertyValue item ?c2 ?l)
(/= ?c1 ?c2))
(PropertyValue disjointWith ?c1 ?c2)))))
%% Note that the following can be inferred from the axioms regarding
"Disjoint" and "subClassOf":
Th5. (PropertyValue subClassOf Disjoint List)
5.1.4. List
%% A list is a sequence.
Ax67. (PropertyValue subClassOf List Seq)
5.1.5. Empty
%% "Empty" and "Nothing" are the same class.
Ax68. (PropertyValue asClass Empty Nothing)
5.1.6. TransitiveProperty
%%"TransitiveProperty" is a class.
Ax69. (Type TransitiveProperty Class)
%% Saying that an object P is a "TransitiveProperty" is equivalent to
saying that P is a property and that P is a transitive relation.
Ax70. (<=> (Type ?p TransitiveProperty)
(and (Type ?p Property)
(forall (?x ?y ?z)
(=> (and (PropertyValue ?p ?x ?y)
(PropertyValue ?p ?y ?z))
(PropertyValue ?p ?x ?z)))))
%% Note that the following can be inferred from the axioms regarding
"TransitiveProperty" and "subClassOf":
Th6. (PropertyValue subClassOf TransitiveProperty Property)
5.1.7. UniqueProperty
%%"UniqueProperty" is a class.
Ax71. (Type UniqueProperty Class)
%% 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.
Ax72. (<=> (Type ?p UniqueProperty)
(and (Type ?p Property)
(forall (?x ?y ?z)
(=> (and (PropertyValue ?p ?x ?y)
(PropertyValue ?p ?x ?y))
(= ?y ?z)))))
%% Note that the following can be inferred from the axioms regarding
"UniqueProperty" and "subClassOf":
Th7. (PropertyValue subClassOf UniqueProperty Property)
5.1.8. UnambiguousProperty
%%"UnambiguousProperty" is a class.
Ax73. (Type UnambiguousProperty 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.
Ax74. (<=> (Type ?p UnambiguousProperty)
(and (Type ?p Property)
(forall (?x ?y ?v)
(=> (and (PropertyValue ?p ?x ?v)
(PropertyValue ?p ?y ?v))
(= ?x ?y)))))
%% Note that the following can be inferred from the axioms regarding
"UnambiguousProperty" and "subClassOf":
Th8. (PropertyValue subClassOf UnambiguousProperty Property)
5.1.9. Restriction
%% "Restriction" is a Class.
Ax75. (Type Restriction Class)
5.1.10. Qualification
%% "Qualification" is a Class.
Ax76. (Type Qualification Class)
5.1.11. Ontology
%% An ontology is a class.
Ax77. (Type Ontology Class)
5.2. Properties
This section axiomatizes the properties that are added to RDF and RDF Schema.
5.2.1. disjointWith
%% "disjointWith" is a property.
Ax78. (Type disjointWith Property)
%% 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.
Ax79. (<=> (PropertyValue disjointWith ?c1 ?c2)
(and (Type ?c1 Class)
(Type ?c2 Class)
(exists (?x) (or (Type ?x ?c1) (Type ?x ?c2)))
(not (exists (?x) (and (Type ?x ?c1) (Type ?x ?c2))))))
%% Note that the following can be inferred from the axioms regarding
"disjointWith", "domain", and "range":
Th9. (PropertyValue domain disjointWith Class)
Th10. (PropertyValue range disjointWith Class)
5.2.2. unionOf
%% "unionOf" is a property.
Ax80. (Type unionOf Property)
%% 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.
Ax81. (<=> (PropertyValue unionOf ?c1 ?l)
(and (Type ?c1 Class)
(Type ?l List)
(forall (?x) (=> (PropertyValue item ?x ?l)
(Type ?x Class)))
(forall (?x)
(<=> (Type ?x ?c1)
(exists (?c2)
(and (PropertyValue item ?c2 ?l)
(Type ?x ?c2)))))))
%% Note that the following can be inferred from the axioms regarding
"unionOf", "domain", and "range":
Th11. (PropertyValue domain unionOf Class)
Th12. (PropertyValue range unionOf List)
5.2.3. disjointUnionOf
%% "disjointUnionOf" is a property.
Ax82. (Type disjointUnionOf Property)
%% 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.
Ax83. (<=> (PropertyValue disjointUnionOf ?c ?l)
(and (PropertyValue unionOf ?c ?l) (Type ?l Disjoint)))
%% Note that the following can be inferred from the axioms regarding
"disjointUnionOf", "unionOf", "domain", and "range":
Th13. (PropertyValue domain disjointUnionOf Class)
Th14. (PropertyValue range disjointUnionOf Disjoint)
5.2.4. intersectionOf
%% "intersectionOf" is a property.
Ax84. (Type intersectionOf Property)
%% 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.
Ax85. (<=> (PropertyValue intersectionOf ?c1 ?l)
(and (Type ?c1 Class)
(Type ?l List)
(forall (?x) (=> (PropertyValue item ?x ?l)
(Type ?x Class)))
(forall (?x)
(<=> (Type ?x ?c1)
(forall (?c2)
(=> (PropertyValue item ?c2 ?l)
(Type ?x ?c2 )))))))
%% Note that the following can be inferred from the axioms regarding
"intersectionOf", "domain", and "range":
Th15. (PropertyValue domain intersectionOf Class)
Th16. (PropertyValue range intersectionOf List)
5.2.5. complementOf
%% "complementOf" is a property.
Ax86. (Type complementOf Property)
%% 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.
Ax87. (<=> (PropertyValue complementOf ?c1 ?c2)
(and (PropertyValue 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":
Th17. (PropertyValue domain complementOf Class)
Th18. (PropertyValue range complementOf Class)
Th19. (complementOf Thing Nothing)
5.2.6. oneOf
%% "oneOf" is a property.
Ax88. (Type one of Property)
%% 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.
Ax89. (<=> (PropertyValue oneOf ?c ?l)
(and (Type ?c Class)
(Type ?l List)
(forall (?x) (<=> (Type ?x ?c)
(PropertyValue item ?x ?l)))))
%% Note that the following can be inferred from the axioms regarding
"oneOf", "domain", and "range":
Th20. (PropertyValue domain oneOf Class))
Th21. (PropertyValue range oneOf List)
5.2.7. asClass
%% Note: There is no definition of "asClass" in the DAMl-ONT spec.
Below is a set of proposed axioms for "asClass".
%% "asClass" is a property.
Ax90. (Type asClass Property)
%% Saying that objects C1 and C2 are "asClass" is equivalent to saying
that C1 and C2 denote the same class.
Ax91. (<=> (PropertyValue asClass ?c1 ?c2)
(and (Type ?c1 Class) (Type ?c2 Class) (= ?c1 ?c2)))
%% Note that the following can be inferred from the axioms regarding
"asClass", "domain", and "range":
Th22. (PropertyValue domain asClass Class)
Th23. (PropertyValue range asClass Class)
5.2.8. first
%% "first" is a property.
Ax92. (Type first Property)
%% The first argument of "first" is a list.
(PropertyValue 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.
Ax93. (<=> (PropertyValue first ?l ?x)
(and (Type ?l List)
(exists (?r) (= ?l (cons ?x ?r))))
%%Note: DAML-ONT seems to need an equivalent of KIF's "cons" as part of
the language.
5.2.9. rest
%% "rest" is a property.
Ax94. (Type rest Property)
%% 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.
Ax95. (<=> (PropertyValue rest ?l ?r)
(and (Type ?l List)
(Type ?r List)
(exists (?x) (= ?l (cons ?x ?r)))))
%% Note that the following can be inferred from the axioms regarding
"oneOf", "domain", and "range":
Th24. (PropertyValue domain rest List))
Th25. (PropertyValue range rest List)
5.2.10. item
%% "item" is a property.
Ax96. (Type item Property)
%% 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.
Ax97. (<=> (PropertyValue item ?l ?x)
(and (Type ?l List)
(or (PropertyValue first ?l ?x)
(exists (?r) (and (PropertyValue rest ?l ?r)
(PropertyValue item ?r ?x))))))
%% Note that the following can be inferred from the axioms regarding
"item", and "domain":
Th26. (PropertyValue domain item List))
5.2.11. cardinality
%% "cardinality" is a property.
Ax98. (Type cardinality Property)
%% Saying that objects P and N are "cardinality" is equivalent to saying
that P is a property and for all objects X, any no repeats list
containing exactly those objects V such that (P X V) is of length N.
Ax99. (<=> (PropertyValue cardinality ?p ?n)
(and (Type ?p Property)
(forall (?x ?vl)
(=> (no-repeats-list ?vl)
(forall (?v)
(<=> (PropertyValue item ?vl ?v)
(PropertyValue ?p ?x ?v)))
(= (length ?vl) ?n)))))
%%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":
Th27. (PropertyValue domain cardinality Property)
Th28. (PropertyValue range cardinality Integer)
Th29. (=> (PropertyValue cardinality ?p ?n) (not (negative ?n)))
5.2.12. maxCardinality
%% "maxCardinality" is a property.
Ax100. (Type maxCardinality Property)
%% 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 any
list containing exactly those objects V such that (P X V) is equal to or
less than N.
Ax101. (<=> (PropertyValue maxCardinality ?p ?n)
(and (Type ?p Property)
(forall (?x ?vl)
(=> (and (no-repeats-list ?vl)
(forall
(?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?x ?v))))
(=< (length ?vl) ?n)))))
%% Note that the following can be inferred from the axioms regarding
"cardinality", "domain", "range", and "length":
Th30. (PropertyValue domain maxCardinality Property)
Th31. (PropertyValue range maxCardinality Integer)
Th32. (=> (PropertyValue maxCardinality ?p ?n) (not (negative ?n)))
5.2.13. minCardinality
%% "minCardinality" is a property.
Ax102. (Type minCardinality Property)
%% Saying that objects P and N are "minCardinality" is equivalent to
saying that P is a property and for all objects X, there exists a no
repeats list of length at least N that contains only objects V such that
(P X V).
Ax103. (<=> (PropertyValue minCardinality ?p ?n)
(and (Type ?p Property)
(forall (?x)
(exists (?vl)
(and (no-repeats-list ?vl)
(forall (?v)
(=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?x ?v)))
(>= (length ?vl) ?n))))))
%% Note that the following can be inferred from the axioms regarding
"minCardinality", "domain", "range", and "length":
Th33. (PropertyValue domain minCardinality Property)
Th34. (PropertyValue range minCardinality Integer)
Th35. (=> (PropertyValue minCardinality ?p ?n) (not (negative ?n)))
5.2.14. inverseOf
%% "inverseOf" is a property.
Ax104. (Type inverseOf Property)
%% Both arguments of "inverseOf" are properties.
(PropertyValue domain inverseOf Property)
(PropertyValue 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.
Ax105. (<=> (PropertyValue inverseOf ?p1 ?p2)
(and (Type ?p1 Property)
(Type ?p2 Property)
(forall (?x1 ?x2)
(<=> (PropertyValue ?p1 ?x1 ?x2)
(PropertyValue ?p2 ?x2 ?x1)))))
%% Note that the following can be inferred from the axioms regarding
"inverseOf", "domain", and "range":
Th36. (PropertyValue domain inverseOf Property)
Th37. (PropertyValue range inverseOf Property)
5.2.15. restrictedBy
%% "restrictedBy" is a property.
Ax106. (Type restrictedBy Property)
%% The first argument of restrictedBy is a class.
Ax107. (PropertyValue domain restrictedBy Class)
%% The second argument of restrictedBy is a restriction.
Ax108. (PropertyValue range restrictedBy Restriction)
5.2.16. onProperty
%% "onProperty" is a property.
Ax109. (Type onProperty Property)
%% The first argument of onProperty is a restriction or a qualification.
Ax110. (=> (PropertyValue onProperty ?rq ?p)
(or (Type ?rq Restriction) (Type ?rq Qualification)))
%% The second argument of onProperty is a property.
Ax111. (PropertyValue range onProperty Property)
5.2.17. toValue
%% "toValue" is a property.
Ax112. (Type toValue Property)
%% The first argument of toValue is a restriction.
Ax113. (PropertyValue 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.
Ax114. (=> (and (PropertyValue restrictedBy ?c ?r)
(PropertyValue onProperty ?r ?p)
(PropertyValue toValue ?r ?v))
(forall (?i) (=> (Type ?i ?c)
(PropertyValue ?p ?i ?v))))
5.2.18. toClass
%% "toClass" is a property.
Ax115. (Type toClass Property)
%% The first argument of toClass is a restriction.
Ax116. (PropertyValue domain toClass Restriction)
%% The second argument of toClass is a class.
Ax117. (PropertyValue 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".
Ax118. (=> (and (PropertyValue restrictedBy ?c1 ?r)
(PropertyValue onProperty ?r ?p)
(PropertyValue toClass ?r ?c2))
(forall (?i) (=> (and (Type ?i ?c1)
(PropertyValue ?p ?i ?v))
(PropertyValue ?v ?c2))))
5.2.19. qualifiedBy
%% "qualifiedBy" is a property.
Ax119. (Type qualifiedBy Property)
%% The first argument of qualifiedBy is a class.
Ax120. (PropertyValue domain qualifiedBy Class)
%% The second argument of qualifiedBy is a qualification.
Ax121. (PropertyValue range qualifiedBy Qualification)
5.2.20. hasValue
%% "hasValue" is a property.
Ax122. (Type hasValue Property)
%% The first argument of hasValue is a qualification.
Ax123. (PropertyValue domain hasValue Qualification)
%% The second argument of hasValue is a class.
Ax124. (PropertyValue 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".
Ax125. (=> (and (PropertyValue qualifiedBy ?c1 ?q)
(PropertyValue onProperty ?q ?p)
(PropertyValue hasValue ?q ?c2))
(forall (?i) (=> (Type ?i ?c1)
(exists (?v)
(and (PropertyValue ?p ?i ?v)
(Type ?v ?c2))))))
%% Note that the following can be inferred from the axioms regarding
"qualifiedBy", "onProperty", "hasValue" and "minCardinality":
Th38. (=> (and (PropertyValue qualifiedBy ?c1 ?q)
(PropertyValue onProperty ?q ?p)
(PropertyValue hasValue ?q ?c2))
(PropertyValue minCardinality ?p 1))
5.2.21. versionInfo
%% "versionInfo" is a property.
Ax126. (Type versionInfo Property)
%% The first argument of "versionInfo" is an ontology.
Ax127. (PropertyValue domain versionInfo Ontology)
5.2.22. imports
%% "imports" is a property.
Ax128. (Type imports Property)
%% Both arguments of "imports" are ontologies.
Ax129. (PropertyValue domain imports Ontology)
Ax130. (PropertyValue range imports Ontology)
5.2.23. equivalentTo
%% "equivalentTo" is a property.
Ax131. (Type equivalentTo Property)
%% 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).
Ax132. (<=> (PropertyValue equivalentTo ?x ?y) (= ?x ?y))
5.2.24. default
%% "default" is a property.
Ax133. (Type default Property)
%% The first argument of "default" is a property.
Ax134. (PropertyValue domain default Property)
Previous versions of this document used additional KIF constructs such as "holds" and sequence
variables not found in other first-order logic languages. Those constructs have been eliminated from the
axiomatization in this version of the document.
The authors would like to thank Pat Hayes for his generous help in debugging earlier versions of this
document.
For more on type see section 3.2.1.
KIF note: "<=>" means "if and only if". Relational sentences in KIF have the form " (
*)". Names whose first character is ``?'' are variables. If no explicit quantifier is specified,
variables are assumed to be universally quantified.
KIF notes: "nil" denotes an empty list. "(listof x)" is a term that denotes the list of length 1 whose first
(and only) item is x. "=" means "denotes the same object in the domain of discourse". "item" is a binary
relation that holds when the object denoted by its second argument is an element of the list denoted by its
first argument. "first" is a unary function whose value is the first element of the list denoted by its
argument. "rest" is a unary function which has a value when its argument is a non-empty list and has as a
value the list consisting of all but the first element of the list denoted by the argument.
KIF note: "=>" means "implies".
KIF note: "/=" means "not equal". I.e., "(/= t1 t2)" is equivalent to "(not (= t1 t2))".
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.
KIF note: "length" is a KIF function that denotes the number of items in the list denoted by the argument
of "length".
KIF note: "integer" and "negative" are KIF relations on numbers.
KIF note: "=<" is the KIF relation for "less than or equal".