An Axiomatic Semantics for RDF, RDF-S, and DAML+OIL
Richard Fikes
Deborah L McGuinness
Knowledge Systems Laboratory
Computer Science Department
Stanford University
January 11, 2001
This document provides an axiomatization for the Resource Description Framework (RDF), RDF Schema (RDF-S), and DAML+OIL 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.
Providing a means of translating RDF, RDF-S, and DAML+OIL descriptions into a first-order predicate calculus logical theory not only specifies the intended meaning of the descriptions, but also produces a representation of the descriptions from which inferences can automatically be made using traditional automatic theorem provers and problem solvers. For example, the DAML+OIL axioms enable a reasoner to infer from the two statements “Class Male and class Female are disjointWith.” and “John is type Male.” that the statement “John is type Female.” is false.
The mapping into predicate calculus 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-S (http://www.w3.org/TR/rdf-schema/)
and DAML+OIL (http://www.daml.org/2000/12/daml+oil-index.html)
are both vocabularies of non-logical symbols added to RDF, the translation of
RDF statements is sufficient for translating RDF-S and DAML+OIL 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+OIL 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-S, or DAML+OIL 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-S, or DAML+OIL).
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 therefore all 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 use of a set theory, 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-S, or DAML+OIL 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-S, and DAML+OIL 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 logically 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
type “Class”.
Ax3.
(Type Resource
Class)
%% If an object P
is type “Property” then P is also type “Resource”. (I.e., properties are resources.)
Ax4.
(=> (Type ?p Property) (Type ?p Resource))[6][7]
%% The first
argument of relation “PropertyValue” is type “Property”.
Ax5.
(=>
(PropertyValue ?p ?s ?o) (Type ?p Property))
%% If an object C
is type “Class” then C is also type “Resource” (i.e., classes are resources),
and no object can be both type “Property” and type “Class” (i.e., properties
and classes are disjoint).
Ax6.
(=> (Type ?c
Class) (Type ?c Resource))
Ax7.
(not (and (Type ?x
Property) (Type ?x Class)))
The class “FunctionalProperty” is not in RDF or RDF-S. We define “FunctionalProperty” only for convenience in axiomatizing other classes and properties.
%% If an object A
is type “FunctionalProperty” then A is also type “Property”. (I.e., functional properties are
properties.)
Ax8.
(=> (Type ?a
FunctionalProperty) (Type ?a Property))
%% If an object FP
is type “FunctionalProperty”, and objects V1 and V2 are both values of FP for
some object, then V1 is equal to V2.
(I.e., a functional property is functional in its value.)
Ax9.
(=> (and (Type
?fp FunctionalProperty)
(PropertyValue ?fp ?s ?v1)
(PropertyValue ?fp ?s ?v2))
(= ?v1 ?v2))
%% “Literal” is
type “Class”.
Ax10. (Type Literal Class)
%% If an object S
is type “Statement”, then S is also type “Resource”. (I.e., statements are resources.)
Ax11. (=> (Type ?s Statement) (Type ?s Resource))
%% If an object ST
is type “Statement”, then there exists a value of “Predicate” for ST, a value
of “Subject” for ST, and a value of “Object” for ST. (I.e., every statement has
a predicate, subject, and object.)
Ax12. (=> (Type Statement ?st)
(exists (?p ?s ?o)
(and (PropertyValue
Predicate ?st ?p)
(PropertyValue Subject
?st ?r)
(PropertyValue Object
?st ?o))))
%% If an object C
is type “Container”, then C is also type “Resource”. (I.e., containers are resources.)
Ax13. (=> (Type ?c Container) (Type ?c Resource))
%% If an object C
is type “Container”, then C is a KIF list.
(I.e., a container is considered to be a list as defined in KIF.)
Ax14. (=> (Type ?c Container) (List ?c))
%% If an object C
is type “Container”, then C is type “Bag” or type “Seq” or type “Alt”. (I.e., a container is a bag, a sequence, or
an alternative.)
Ax15. (=> (Type ?c Container)
(or (Type ?c Bag)
(Type ?c Seq)
(Type ?c Alt)))
%% If an object B
is type “Bag”, then B is also type “Container”. (I.e., bags are containers.)
Ax16. (=> (Type ?b Bag) (Type ?b Container))
%% If an object S
is type “Seq”, then S is also type “Container”. (I.e., sequences are containers.)
Ax17. (=> (Type ?s Seq) (Type ?s Container))
%% No object X is
both type “Bag” and type “Seq”. (I.e.,
bags and sequences are disjoint.)
Ax18. (not (and (Type ?x Bag) (Type ?x Seq)))
%% If an object A
is type “Alt”, then A is also type “Container”. (I.e., alternatives are containers.)
Ax19. (=> (Type ?a Alt) (Type ?a Container))
%% If an object C
is type “ContainerMembershipProperty”, then C is also type “Property”. (I.e., container membership properties are
properties.)
Ax20. (=> (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 type “Property”. (I.e., “type” is a property.)
Ax21. (Type type Property)
%% The first
argument of “Type” is a resource and the second argument of “Type” is a class.
Ax22. (=> (Type ?r ?c) (and (Type ?r Resource)
(Type ?c Class)))[8]
%% “Subject” is
type “FunctionalProperty”, and if an object SB is the value of “Subject” for an
object ST, then ST is type “Statement” and SB is type “Resource”. (I.e., every statement has exactly one
subject, and that subject is a resource.)
Ax23. (Type Subject FunctionalProperty)
Ax24. (=> (PropertyValue Subject ?st ?sb)
(and (Type ?st Statement) (Type ?sb
Resource)))
%% “Predicate” is
type “FunctionalProperty”, and if an object P is the value of “Predicate” for
an object ST, then P is type “Property” and ST is type “Statement”. (I.e., every statement has exactly one
predicate, and that predicate is a property.)
Ax25. (Type Predicate FunctionalProperty)
Ax26. (=> (PropertyValue Predicate ?st ?p)
(and (Type ?st Statement) (Type ?p
Property)))
%% “Object” is
type “FunctionalProperty”, and if an object O is the value of “Object” for an
object ST, then O is either type “Resource” or type “Literal” and ST is type
“Statement”. (I.e., every statement has
exactly one object, and that object is either a resource or a literal.)
Ax27. (Type Object FunctionalProperty)
Ax28. (=> (PropertyValue Object ?st ?o)
(and (Type ?st Statement)
(or (Type ?o Resource) (Type ?o
Literal))))
%% “value” is type
“Property”, and if an object V is a value of “value” for an object SV, then SV
is type “Resource” and V is either type “Resource” or type “Literal”.
Ax29. (Type value Property)
Ax30. (=> (PropertyValue value ?sv ?v)
(and (Type ?sv Resource)
(or (Type ?v Resource) (Type ?v
Literal))))
%% For each
positive integer N, “_N” is type “FunctionalProperty”, and if an object O is
the value of “_N” for an object C, then C is type “Collection”. (The _N of a collection is intended to be
the Nth element of that collection.)
Ax31. (Type FunctionalProperty _1)
Ax32. (=> (PropertyValue _1 ?c ?o) (Type
Collection ?c))
and similarly for
_2, _3, etc.
RDF-S is a collection of classes and properties that is added to RDF. Statements in RDF-S are RDF statements.
This section axiomatizes the classes that are added to RDF in RDF-S.
“ConstraintResource” is a class of RDF-S constructs involved in the expression of constraints.
%% “Resource” is a
value of “subClassOf” for “ConstraintResource”. (I.e., constraint resources are resources.)
Ax33. (PropertyValue subClassOf
ConstraintResource Resource)
%% An object CP is
type “ConstraintProperty” if and only if it is type “ConstraintResource” and
type “Property”. (I.e., constraint
properties are exactly those constraint resources that are also properties.)
Ax34. (<=> (Type ?cp ConstraintProperty)
(and (Type ?cp ConstraintResource)
(Type ?cp Property)))
This section axiomatizes the properties that are added to RDF in RDF-S.
%% “subClassOf” is
type “Property”.
Ax35. (Type subClassOf Property)
%% If an object
CSUPER is a value of “subClassOf” for an object CSUB, then CSUPER is type
“Class”, CSUB is type “Class”, CSUB is not CSUPER, and if an object X is type
CSUB then it is also type CSUPER.
(I.e., the arguments of subClassOf are classes, and objects in a
subclass are also in the superclass.)
Ax36. (=> (PropertyValue subClassOf ?csub
?csuper)
(and (Type ?csub Class)
(Type ?csuper Class)
(\= ?csub ?csuper)
(forall (?x) (=> (Type ?x ?csub) (Type ?x ?csuper)))))
%% “subPropertyOf”
is type “Property”.
Ax37. (Type subPropertyOf Property)
%% If an object
SUPERP is a value of “subPropertyOf” of an object SUBP, then SUBP is type
“Property”, SUPERP is type “Property”, and if an object V is a value of SUBP
for an object O then V is also a value of SUPERP for O. (I.e., if a subProperty has a value V for an
object O, then the superproperty also has value V for O.)
Ax38. (=> (PropertyValue subPropertyOf ?subP ?superP)
(and (Type ?subP Property)
(Type ?superP Property)
(forall (?o ?v) (=>
(PropertyValue ?subP ?o ?v)
(PropertyValue ?superP ?o ?v)))))
%% “seeAlso” is
type “Property”, and “Resource” is a value of both “domain” and “range” for
“seeAlso. (I.e., “seeAlso” is a
property whose arguments are resources.)
Ax39. (Type seeAlso Property)
Ax40. (PropertyValue domain seeAlso Resource)
Ax41. (PropertyValue range seeAlso Resource)
%% “seeAlso” is a
value of “subPropertyOf” for “isDefinedBy”.
(I.e., “isDefinedBy” is a subproperty of “seeAlso”.)
Ax42. (PropertyValue subPropertyOf isDefinedBy
seeAlso)
%% “comment” is
type “Property”, and “Literal” is the value of “range” for “comment”. (I.e., “comment” is a property whose value
is a literal.)
Ax43. (Type comment Property)
Ax44. (PropertyValue range comment Literal)
%% “label” is type
“Property”, and “Literal” is the value of “range” for “label”. (I.e., “label” is a property whose value is
a literal.)
Ax45. (Type label Property)
Ax46. (PropertyValue range label Literal)
%% “Property” is a
value of “subClassOf” for “ConstraintProperty”. (I.e., constraint properties are properties.)
Ax47. (PropertyValue subClassOf
ConstraintProperty Property)
%% “range” is type
“ConstraintProperty” and type “FunctionalProperty”.
Ax48. (Type range ConstraintProperty)
Ax49. (Type range FunctionalProperty)
%% If an object R
is the value of “range” for an object P, then P is type “Property”, R is type
“Class”, and if an object Y is a value of P then Y is type R. (I.e., if R is the range of P, then P is a
property, R is a class, and every value of P is an R.)
Ax50. (=> (PropertyValue range ?p ?r)
(and (Type ?p Property)
(Type ?r Class)
(forall (?x ?y)
(=> (PropertyValue
?p ?x ?y) (Type ?y ?r)))))
%% 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
type “ConstraintProperty”.
Ax51. (Type domain ConstraintProperty)
%% If an object D
is a value of “domain” for an object P, then P is type “Property”, D is type
“Class”, and if P has a value for an object X then X is type D. (I.e., if D is a domain of P, then P is a
property, D is a class, and every object that has a value of P is a D.)
Ax52. (=> (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+OIL is a collection of classes, properties, and objects that is added to RDF and RDF-S. Statements in DAML+OIL are RDF statements.
This section axiomatizes the classes that are added to RDF and RDF-S.
%% If an object C
is type “class”, then if NC is the value of “complementOf” for C and L is a two
element list containing C and NC, then L is a value of “unionOf” for
“Thing”. (I.e., “Thing” is the union of
any class and its complement.)
Ax53. (=> (Type ?c Class)
(forall (?nc ?l)
(=> (and (PropertyValue
complementOf ?c ?nc)
(Type ?l List)
(PropertyValue item
?l ?c)
(PropertyValue item
?l ?nc)
(forall (?x) (=>
(PropertyValue item ?l ?x)
(or (= ?x ?c)
(= ?x ?nc)))))
(PropertyValue unionOf
Thing ?l))))
%% “Nothing” is
the value of “complementOf” for “Thing”.
(I.e., “Nothing” is the complement of “Thing”.)
Ax54. (PropertyValue complementOf Thing Nothing)
%% “Disjoint” is
type “Class”.
Ax55. (Type Disjoint Class)
%% Saying that an
object is type “Disjoint” is logically equivalent to saying that the object is
type “List”, that every item in the list is type “Class”, and that the classes
in the list are pairwise joint.
Ax56. (<=> (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)
(not (= ?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)
%% “Restriction”
is type “Class”.
Ax57. (Type Restriction Class)
%% “Integer” is a
value of “subClassOf” for “NonNegativeInteger”. (I.e., non-negative integers are integers.)
Ax58. (subClassOf NonNegativeInteger Integer)
%%
“TransitiveProperty” is type “Class”.
Ax59. (Type TransitiveProperty Class)
%% Saying that an
object P is type “TransitiveProperty” is logically equivalent to saying that P
is a property and that if an object Y is a value of P for an object X and an
object Z is a value of P for Y then Z is a value of P for X.
Ax60. (<=> (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 type “Class”.
Ax61. (Type UniqueProperty Class)
%% Saying that an
object P is type “UniqueProperty” is logically equivalent to saying that P is
type “Property” and that if an object Y is a value of P for an object X and an
object Z is a value of P for X then Y is equal to Z (i.e., then Y and Z are the
same object).
Ax62. (<=> (Type ?p UniqueProperty)
(and (Type ?p Property)
(forall (?x ?y ?z)
(=> (and
(PropertyValue ?p ?x ?y)
(PropertyValue ?p ?x ?z))
(= ?y ?z)))))
%% Note that the
following can be inferred from the axioms regarding “UniqueProperty” and
“subClassOf”:
Th7.
(PropertyValue
subClassOf UniqueProperty Property)
%%”UnambiguousProperty”
is type “Class”.
Ax63. (Type UnambiguousProperty Class)
%% Saying that an
object P is type “UnambiguousProperty” is logically equivalent to saying that P
is type “Property” and that if an object V is a value of P for an object X and
V is a value of P for an object Y then X is equal to Y (i.e., then X and Y are
the same object).
Ax64. (<=> (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)
%% “Seq” is a
value of “subClassOf” for “List”. (I.e.,
lists are sequences.)
Ax65. (PropertyValue subClassOf List Seq)
%% An ontology is
type “Class”.
Ax66. (Type Ontology Class)
This section axiomatizes the properties that are added to RDF and RDF-S.
%% “equivalentTo”
is type “Property”.
Ax67. (Type equivalentTo Property)
%% An object Y is
a value of “equivalentTo” for an object X if and only if X is equal to Y. (I.e., saying that objects X and Y are
“equivalentTo” is logically equivalent to saying that X and Y denote the same
object.)
Ax68. (<=> (PropertyValue equivalentTo ?x
?y) (= ?x ?y))
%% The values of
“subPropertyOf” for “sameClassAs” include “equivalentTo” and “subClassOf”. (I.e., “sameClassAs” is “equivalentTo” for
classes, and two classes that are the same are also subclasses of each other.)
Ax69. (PropertyValue subPropertyOf sameClassAs
equivalentTo)
Ax70. (PropertyValue subPropertyOf sameClassAs
subClassOf)
%% The values of
“subPropertyOf” for “samePropertyAs” include “equivalentTo” and
“subPropertyOf”. (I.e., “samePropertyAs”
is “equivalentTo” for properties, and two properties that are the same are also
subproperties of each other.)
Ax71. (PropertyValue subPropertyOf samePropertyAs
equivalentTo)
Ax72. (PropertyValue subPropertyOf samePropertyAs
subPropertyOf)
%% “disjointWith”
is type “Property”.
Ax73. (Type disjointWith Property)
%% Saying that an
object C2 is a value of “disjointWith” for an object C1 is logically equivalent
to saying that C1 is type “Class”, C2 is type “Class”, and that no object X is
both type C1 and type C2.
Ax74. (<=> (PropertyValue disjointWith ?c1
?c2)
(and (Type ?c1 Class)
(Type ?c2 Class)
(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.
Ax75. (Type unionOf Property)
%% Saying that an
object L is a value of “unionOf” for an object C1 is logically equivalent to
saying that C1 is type “Class”, L is type “List”, every item in list L is type
“Class”, and the objects of type C1 are exactly the objects that are of type
one or more of the classes in the list L.
Ax76. (<=> (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 type “Property”.
Ax77. (Type disjointUnionOf Property)
%% Saying that an
object L is a value of “disjointUnionOf” for an object C is logically
equivalent to saying that L is type “Disjoint” and L is a value of “unionOf”
for C. (I.e., an object C is a disjoint
union of an object L if and only if L is a list of pairwise disjoint classes
and C is the union of the list L of classes.)
Ax78. (<=> (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 type “Property”.
Ax79. (Type intersectionOf Property)
%% Saying that an
object L is a value of “intersectionOf” for an object C1 is logically equivalent
to saying that C1 is type “Class”, L is type “List”, all of the items in list L
are type “Class”, and the objects that are type C1 are exactly those objects
that are type all of the classes in list L.
Ax80. (<=> (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 type “Property”.
Ax81. (Type complementOf Property)
%% Saying that an
object C2 is a value of “complementOf” for an object C1 is logically equivalent
to saying that C1 and C2 are disjoint classes and all objects are either type
C1 or type C2.
Ax82. (<=> (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”, and “range”:
Th17. (PropertyValue domain complementOf Class)
Th18. (PropertyValue range complementOf Class)
Th19. (PropertyValue complementOf Thing Nothing)
%% “oneOf” is type
“Property”.
Ax83. (Type oneOf Property)
%% Saying that an
object L is a value of “oneOf” for an object C is logically equivalent to
saying that C is type “Class”, L is type “List”, and the objects that are type C
are exactly the objects that are values of “item” for L. (I.e., saying that C is “oneOf” L is saying
that C is a class, L is a list, and the objects of type C are the objects on
the list L.)
Ax84. (<=> (PropertyValue oneOf ?c ?l)
(and (Type ?c Class)
(Type ?l List)
(forall (?x) (<=> (Type
?x ?c)
(PropertyValue item ?l ?x)))))
%% 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)
%% “onProperty” is
type “Property”.
Ax85. (Type onProperty Property)
%% “Ristriction”
is a value of “domain” for “onProperty”.
(I.e., the first argument of onProperty is a restriction.)
Ax86. (PropertyValue domain onProperty
Restriction)
%% “Property” is
the value of “range” for “onProperty”.
(I.e., the second argument of onProperty is a property.)
Ax87. (PropertyValue range onProperty Property)
%% “toClass” is
type “Property”.
Ax88. (Type toClass Property)
%% “Restriction”
is a value of “domain” for “toClass”.
(I.e., the first argument of toClass is a restriction.)
Ax89. (PropertyValue domain toClass Restriction)
%% “Class” is the
value of “range” for “toClass”. (I.e.,
the second argument of toClass is a class.)
Ax90. (PropertyValue range toClass Class)
%% If a property P
is a value of “onProperty” for a restriction R and a class C is a value of
“toClass” for R, then an object I is type R if and only if every value of P for
I is type C. (I.e., a “toClass”
restriction of C on a property P is the class of all objects I such that all
values of P for I are type C.)
Ax91. (=> (and (PropertyValue onProperty ?r
?p)
(PropertyValue toClass ?r ?c))
(forall (?i) (<=> (Type ?i ?r)
(forall (?j) (=> (PropertyValue ?p ?i ?j)
(Type ?j ?c))))))
%% “hasValue” is
type “Property”.
Ax92. (Type hasValue Property)
%% “Restriction”
is a value of “domain” for “hasValue”.
(I.e., the first argument of hasValue is a restriction.)
Ax93. (PropertyValue domain hasValue Restriction)
%% If a property P
is a value of “onProperty” for a restriction R and an object V is a value for
“hasValue” for R, then an object I is type R if and only if V is a value of P
for I. (I.e., a “hasValue” restriction
of V on a property P is the class of all objects that have V as a value of P.)
Ax94. (=> (and (PropertyValue onProperty ?r
?p)
(PropertyValue hasValue ?r ?v))
(forall (?i) (<=> (Type ?i ?r)
(PropertyValue ?p ?i ?v))))
%% Note that the
following can be inferred from the axioms regarding “qualifiedBy”,
“onProperty”, “hasValue” and “minCardinality”:
Th22. (=> (and (PropertyValue qualifiedBy ?c1
?q)
(PropertyValue onProperty ?q
?p)
(PropertyValue hasValue ?q
?c2))
(PropertyValue minCardinality ?p 1))
%% “hasClass” is
type “Property”.
Ax95. (Type hasClass Property)
%% “Restriction”
is a value of “domain” for “hasClass”.
(I.e., the first argument of hasClass is a restriction.)
Ax96. (PropertyValue domain hasClass Restriction)
%% “Class” is the
value of “range” for “hasClass”. (I.e.,
the second argument of hasClass is a class.)
Ax97. (PropertyValue range hasClass Class)
%% If a property P
is a value of “onProperty” for a restriction R and a class C is a value of
“hasClass” for R, then an object I is type R if and only if there exists a
value of P for I that is type C. (I.e.,
a “hasClass” restriction of C on a property P is the class of all objects I
which have a value of P that is type C.)
Ax98. (=> (and (PropertyValue onProperty ?r
?p)
(PropertyValue hasClass ?r ?c))
(forall (?i) (<=> (Type ?i ?r)
(exists (?j) (and
(PropertyValue ?p ?i ?j)
(Type ?j ?c))))))
%%
“minCardinality” is type “Property”.
Ax99. (Type minCardinality Property)
%% “Restriction”
is a value of “domain” for “minCardinality”.
(I.e., the first argument of minCardinality is a restriction.)
Ax100.(PropertyValue domain minCardinality
Restriction)
%%
“NonNegativeInteger” is the value of “range” for “minCardinality”. (I.e., the second argument of minCardinality
is a non-negative integer.)
Ax101.(PropertyValue range minCardinality
NonNegativeInteger)
%% If a property P is a value of “onProperty” for a restriction R and a non-negative integer N is a value of “minCardinality” for R, then an object I is type R if and only if there is a “no-repeats-list