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.html
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.[1] 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]
We define the following KIF relations for use in representing RDF, RDF Schema, and DAML-ONT descriptions in KIF.
“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)”.
“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[3]
?s ?o))[4]
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)))))[5]
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)”.
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.
All things being described by RDF expressions are called resources.
%% “Resource” is a
class.
Ax3.
(Type Resource
Class)
%% “Property” is a
subclass of “Resource”.
Ax4.
(Type Property
Class)
Ax5.
(=> (Type ?p
Property) (Type ?p Resource))[6]
%% “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)))
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))
%% “Literal” is a
class.
Ax12. (Type Literal Class)
%% “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))))
%% “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)))
%% A bag is a
container.
Ax20. (Type Bag Class)
Ax21. (=> (Type ?b Bag) (Type ?b Container))
%% 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)))
%% An alternative
is a container.
Ax25. (Type Alt Class)
Ax26. (=> (Type ?a Alt) (Type ?a Container))
%% A container
membership property is a property.
Ax27. (Type ContainerMembershipProperty Class)
Ax28. (=> (Type ?c
ContainerMembershipProperty) (Type ?c Property))
This section axiomatizes the properties that are included in RDF.
“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)))
%% “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)))
%% “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)))
%% “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))))
%% “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))))
%% 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.
RDF Schema is a collection of classes and properties that is added to RDF. Statements in RDF Schema are RDF statements.
This section axiomatizes the classes that are added to RDF in RDF Schema.
“ConstraintResource” is a class of RDF schema constructs involved in the expression of constraints.
%% Constraint
resources are resources.
Ax41. (subClassOf ConstraintResource Resource)
%% Constraint
properties are those constraint resources that are also properties.
Ax42. (<=> (Type ?cp ConstraintProperty)
(and (Type ?cp ConstraintResource)
(Type ?cp Property)))
This section axiomatizes the properties that are added to RDF in RDF Schema.
%% “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)))))
%% “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)))))
%% “seeAlso” is a
property whose arguments are resources.
Ax47. (Type seeAlso Property)
Ax48. (PropertyValue domain seeAlso Resource)
Ax49. (PropertyValue range seeAlso Resource)
%% “isDefinedBy”
is a subproperty of “seeAlso”.
Ax50. (PropertyValue subProperty isDefinedBy
seeAlso)
%% “comment” is a
property whose value is a literal.
Ax51. (Type comment Property)
Ax52. (=> (PropertyValue comment ?s ?l) (Type ?l
Literal))
%% “label” is a
property whose value is a literal.
Ax53. (Type label Property)
Ax54. (=> (PropertyValue label ?s ?l) (Type ?l
Literal))
%% Constraint
properties are properties.
Ax55. (=> (Type ?x ConstraintProperty) (Type
?x Property))
%% “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)
%% “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)
DAML-ONT is a collection of classes and properties that is added to RDF and RDF-Schema. Statements in DAML-ONT are RDF statements.
This section axiomatizes the classes that are added to RDF and RDF Schema.
%% “Thing” is a
Class.
Ax61. (Type Thing Class)
%% Every object is
type Thing.
Ax62. (Type ?x Thing)
%% “Nothing” is a
Class.
Ax63. (Type Nothing Class)
%% No object is
type Nothing.
Ax64. (not (Type ?x Nothing))
%% A “Disjoint” is
a “Class”.
Ax65. (Type Disjoint Class)
Ax65.
%% 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)))))[7]
%% Note that the
following can be inferred from the axioms regarding “Disjoint” and
“subClassOf”:
Th5.
(PropertyValue
subClassOf Disjoint List)
%% A list is a
sequence.
Ax67. (PropertyValue subClassOf List Seq)
%% “Empty” and
“Nothing” are the same class.
Ax68. (PropertyValue asClass Empty Nothing)
%%”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)
%%”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)
%%”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)
%% “Restriction”
is a Class.
Ax75. (Type Restriction Class)
%% “Qualification”
is a Class.
Ax76. (Type Qualification Class)
%% An ontology is
a class.
Ax77. (Type Ontology Class)
This section axiomatizes the properties that are added to RDF and RDF Schema.
%% “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)
%% “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)
%% “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)
%%
“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)
%% “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)
%% “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)
%% 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)
%% “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))))[8]
%%Note: DAML-ONT
seems to need an equivalent of KIF’s “cons” as part of the language.
%% “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)
%% “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))
%% “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)))))[9]
%%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)))[10]
%%
“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)))))[11]
%% 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)))
%%
“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)))
%% “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)
%% “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)
%% “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)
%% “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))))
%% “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))))
%% “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)
%% “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))
%% “versionInfo”
is a property.
Ax126.(Type versionInfo Property)
%% The first
argument of “versionInfo” is an ontology.
Ax127.(PropertyValue domain versionInfo Ontology)
%% “imports” is a
property.
Ax128.(Type imports Property)
%% Both arguments
of “imports” are ontologies.
Ax129.(PropertyValue domain imports Ontology)
Ax130.(PropertyValue range imports Ontology)
%% “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))
%% “default” is a
property.
Ax133.(Type default Property)
%% The first
argument of “default” is a property.
Ax134.(PropertyValue domain default Property)
[1] 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.
[2] The authors would like to thank Pat Hayes for his generous help in debugging earlier versions of this document.
[3] For more on type see section 3.2.1.
[4] KIF note: “<=>” means “if and only if”. Relational sentences in KIF have the form “ (<relation name> <argument>*)”. Names whose first character is ``?'' are variables. If no explicit quantifier is specified, variables are assumed to be universally quantified.
[5] 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.
[6] KIF note: “=>” means “implies”.
[7] KIF note: “/=” means “not equal”. I.e., “(/= t1 t2)” is equivalent to “(not (= t1 t2))”.
[8] 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.
[9] KIF note: “length” is a KIF function that denotes the number of items in the list denoted by the argument of “length”.
[10] KIF note: “integer” and “negative” are KIF relations on numbers.
[11] KIF note: “=<” is the KIF relation for “less than or equal”.