An Axiomatic Semantics for RDF, RDF-S, and DAML+OIL
Richard Fikes
Deborah L McGuinness
Knowledge Systems Laboratory
Computer Science Department
Stanford University
October 2001
1. Introduction
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/2001/03/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.
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.
The axioms are designed to reflect the layering of RDF, RDF-S, and DAML+OIL in the sense
that the axioms for RDF do not use the properties or classes of RDF-S or DAML+OIL, the
axioms for RDF-S use the properties and classes of RDF but do not use the properties or
classes of DAML+OIL, and the axioms for DAML+OIL use the properties and classes of both
RDF and RDF-S.
We have also included in this document a set of theorems inferable from the axioms. These
theorems are intended to facilitate the use of the axioms for automatic reasoning. They are all
either (1) RDF statements that can assumed to be included in any knowledge base, (2) Horn
clauses with RDF statements or evaluable constraints as atoms, or (3) implications in which a
conjunction of atoms (i.e., RDF statements or evaluable constraints) implies FALSE. Each
theorem is provable from the axioms that precede it in the document.
In order to make this document more operational, we also point to two files available online:
one contains all of the kif axioms and the other contains all of the kif theorems. 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-S, and DAML+OIL
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".
%% Relation "Type" holds for objects S and O if and only if relation
"PropertyValue" holds for objects "type", S, and O.
(<=> (Type ?s ?o) (PropertyValue type ?s ?o)) [Type axiom 1]
2.3. FunctionalProperty
The relation "FunctionalProperty" is used in the axiomatization of properties in RDF and RDF-
S.
%% An object FP is "FunctionalProperty" if and only if FP is type
"Property" and if objects V1 and V2 are both values of FP for some
object, then V1 is equal to V2. (I.e., functional properties are those
properties that are functional in their values.)
(<=> (FunctionalProperty ?fp)
(and (Type ?fp Property)
(forall (?s ?v1 ?v2)
(=> (and (PropertyValue ?fp ?s ?v1)
(PropertyValue ?fp ?s ?v2))
(= ?v1 ?v2))))) [FunctionalProperty axiom 1]
2.4. DisjointAll
The relation DisjointAll is used in the axiomatization of the DAML+OIL property
"disjointWith".
%% An object L is "DisjointAll" if and only if L is type "List" and when
L has a value F for property "first" and a value R for property "rest"
then F is disjoint from every C that is a value of "item" for R and R is
"DisjointAll". (I.e., a list L is "DisjointAll" if and only each pair
of its items is disjoint.)
(<=> (DisjointAll ?l)
(and (Type ?l List)
(or (= ?l nil)
(forall (?f ?r)
(=> (and (PropertyValue first ?l ?f)
(PropertyValue rest ?l ?r))
(and (forall (?c)
(=> (PropertyValue item ?r ?c)
(PropertyValue
disjointWith ?f ?c)))
(DisjointAll
?r))))))) [DisjointAll axiom 1]
2.5. NoRepeatsTuple
The length of tuples with no repeating elements is used in the axiomatization of DAML+OIL
cardinality properties. Such tuples and their length are defined by defining the empty tuple
EmptyTuple, the binary relation Item, the unary functions First, Rest, and Length, the binary
functions Cons, and the unary relation NoRepeatsTuple. The intended interpretation of those
relations is that Item relates a tuple to each of its elements, First maps a nonempty tuple to its
first element, Rest relates a nonempty tuple to the tuple consisting of its 2nd through last
elements, Cons maps an element and a tuple to the result of inserting the element at the
beginning of the tuple, Length maps a tuple to the number of elements it has, and
NoRepeatsTuple is true of tuples that have no repeating elements.
%% Item is a binary relation that relates a tuple to its elements. X is
an item of tuple T if and only if T is not the EmptyTuple and either X
is the first of T or X is an item of the rest of T.
(not (Item ?t EmptyTuple)) [NoRepeatsTuple axiom 1]
(<=> (Item ?t (Cons ?x ?r))
(or (= ?t ?x) (Item ?t ?r)))) [NoRepeatsTuple axiom 2]
%% The length of a tuple is the number of elements in the tuple. L is
the length of tuple T if and only if either T is the empty tuple and L
is 0 or L is 1 plust the length of the rest of T.
(<=> (= (Length ?t) 0) (= ?t EmptyTuple)) [NoRepeatsTuple axiom 3]
(= (Length (Cons ?x ?t)) (+ 1 (Length ?t))) [NoRepeatsTuple axiom 4]
%% A NoRepeatsTuple is a tuple for which no item occurs more than once.
T is a NoRepeatsTuple if and only if T is EmptyTuple, EmptyTuple is the
rest of T, or the first of T is not an item of the rest of T and the
rest of T is a NoRepeatsTuple.
(<=> (NoRepeatsTuple ?t)
(or (= ?t EmptyTuple)
(= (Rest ?t) EmptyTuple)
(and (not (Item (First ?t) (Rest ?t))
(NoRepeatsTuple (Rest ?t))))) [NoRepeatsTuple axiom 5]
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)".
The default namespace for the classes and properties defined in this section is
http://www.w3.org/1999/02/22-rdf-syntax-ns#.
3.1. Classes
This section axiomatizes the classes that are included in RDF.
3.1.1. Resource
All things being described by RDF expressions are called resources.
%% "Resource" is type "rdfs:Class".
(Type Resource rdfs:Class) [Resource axiom 1]
3.1.2. Property
%% The first argument of relation "PropertyValue" is type "Property".
(=> (PropertyValue ?p ?s ?o) (Type ?p Property)) [Property axiom 1]
3.1.3. rdfs:Class
This class is prefixed with "rdfs" to indicate that it is from the namespace
http://www.w3.org/2000/01/rdf-schema# and to distinguish it from "Class" as defined in
DAML+OIL.
%% No object can be both type "Property" and type "rdfs:Class" (i.e.,
properties and RDF-S classes are disjoint).
(not (and (Type ?x Property) (Type ?x rdfs:Class))) [rdfs:Class axiom 1]
3.1.4. Literal
%% "Literal" is type "rdfs:Class".
(Type Literal rdfs:Class) [Literal axiom 1]
3.1.5. Statement
%% 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.)
(=> (Type ?st Statement)
(exists (?p ?r ?o)
(and (PropertyValue predicate ?st ?p)
(PropertyValue subject ?st ?r)
(PropertyValue object ?st ?o)))) [Statement axiom 1]
3.1.6. Container, Bag, Seq, and Alt
%% 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.)
(=> (Type ?c Container) (List ?c)) [Container axiom 1]
%% An object C is type "Container" if and only if C is type "Bag" or
type "Seq" or type "Alt". (I.e., a container is a bag, a sequence, or
an alternative.)
(<=> (Type ?c Container)
(or (Type ?c Bag) (Type ?c Seq) (Type ?c Alt))) [Container axiom 2]
3.1.7. ContainerMembershipProperty
%% If an object C is type "ContainerMembershipProperty", then C is also
type "Property". (I.e., a container membership property is a property.)
(=> (Type ?c ContainerMembershipProperty)
(Type ?c Property)) [ContainerMembershipProperty axiom 1]
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 type "Property". (I.e., "type" is a property.)
(Type type Property) [type axiom 1]
%% The first argument of "Type" is a resource and the second argument of
"Type" is a class.
(=> (Type ?r ?c)
(and (Type ?r Resource) (Type ?c rdfs:Class))) [type axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(=> (Type ?p Property) (Type ?p Resource)) [type theorem 1]
(=> (Type ?c rdfs:Class) (Type ?c Resource)) [type theorem 2]
(=> (Type ?s Statement) (Type ?s Resource)) [type theorem 3]
(=> (Type ?c Container) (Type ?c Resource)) [type theorem 4]
(Type Property rdfs:Class) [type theorem 5]
3.2.2. subject
%% "subject" is "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.)
(FunctionalProperty subject) [subject axiom 1]
(=> (PropertyValue subject ?st ?sb)
(and (Type ?st Statement) (Type ?sb Resource))) [subject axiom 2]
3.2.3. predicate
%% "predicate" is "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.)
(FunctionalProperty predicate) [predicate axiom 1]
(=> (PropertyValue predicate ?st ?p)
(and (Type ?st Statement) (Type ?p Property))) [predicate axiom 2]
3.2.4. object
%% "object" is "FunctionalProperty", and if an object O is the value of
"object" for an object ST, then O is type "Resource" and ST is type
"Statement". (I.e., every statement has exactly one object, and that
object is a resource.)
(FunctionalProperty object) [object axiom 1]
(=> (PropertyValue object ?st ?o)
(and (Type ?st Statement) (Type ?o Resource))) [object axiom 2]
3.2.5. value
%% "value" is type "Property", and if an object V is a value of "value"
for an object SV, then SV and V are each type "Resource".
(Type value Property) [value axiom 1]
(=> (PropertyValue value ?sv ?v)
(and (Type ?sv Resource) (Type ?v Resource))) [value axiom 2]
3.2.6. _1, _2, _3, …
%% For each positive integer N, "_N" is "FunctionalProperty", and if an
object O is the value of "_N" for an object C, then C is type
"Container". (The _N of a container is intended to be the Nth element
of that container.)
(FunctionalProperty _1) [_N axiom 1]
(=> (PropertyValue _1 ?c ?o) (Type ?c Container)) [_N axiom 2]
and similarly for _2, _3, etc.
4. RDF-S
RDF-S is a collection of classes and properties that is added to RDF. Statements in RDF-S
are RDF statements.
The default namespace for the classes and properties defined in this section is
http://www.w3.org/2000/01/rdf-schema#.
4.1. Classes
This section axiomatizes the classes that are added to RDF in RDF-S.
4.1.1. ConstraintResource
%% "Resource" is a value of "subClassOf" for "ConstraintResource".
(I.e., a constraint resource is a resource.)
(PropertyValue
subClassOf ConstraintResource Resource) [ConstraintResource axiom 1]
4.1.2. ConstraintProperty
%% 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.)
(<=> (Type ?cp ConstraintProperty)
(and (Type ?cp ConstraintResource)
(Type ?cp Property))) [ConstraintProperty axiom 1]
4.1.3. NonNegativeInteger
%% An object of type "NonNegativeInteger" is an integer.
(=> (Type ?n NonNegativeInteger)
(Integer ?n)) [NonNegativeInteger axiom 1]
4.2. Properties
This section axiomatizes the properties that are added to RDF in RDF-S.
4.2.1. subClassOf
%% "subClassOf" is type "Property".
(Type subClassOf Property) [subClassOf axiom 1]
%% An object CSUPER is a value of "subClassOf" for an object CSUB if and
only if CSUPER is type "rdfs:Class", CSUB is type "rdfs: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.)
(<=> (PropertyValue subClassOf ?csub ?csuper)
(and (Type ?csub rdfs:Class)
(Type ?csuper rdfs:Class)
(forall (?x) (=> (Type ?x ?csub)
(Type ?x ?csuper))))) [subClassOf axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue subClassOf Property Resource) [subClassOf theorem 1]
(PropertyValue subClassOf rdfs:Class Resource) [subClassOf theorem 2]
(PropertyValue subClassOf Statement Resource) [subClassOf theorem 3]
(PropertyValue subClassOf Bag Container) [subClassOf theorem 4]
(PropertyValue subClassOf Seq Container) [subClassOf theorem 5]
(PropertyValue subClassOf Alt Container) [subClassOf theorem 6]
(PropertyValue subClassOf
ContainerMembershipProperty
Property) [subClassOf theorem 7]
(=> (and (PropertyValue subClassOf ?csub ?csuper)
(Type ?x ?csub))
(Type ?x ?csuper)) [subClassOf theorem 8]
4.2.2. subPropertyOf
%% An object SUPERP is a value of "subPropertyOf" of an object SUBP if
and only if 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.)
(<=> (PropertyValue subPropertyOf ?subP ?superP)
(and (Type ?subP Property)
(Type ?superP Property)
(forall (?o ?v)
(=> (PropertyValue ?subP ?o ?v)
(PropertyValue
?superP ?o ?v))))) [subPropertyOf axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(=> (and (PropertyValue subPropertyOf ?subP ?superP)
(PropertyValue ?subP ?o ?v))
(PropertyValue ?superP ?o ?v)) [subPropertyOf theorem 1]
4.2.3. seeAlso
%% "Resource" is a value of both "domain" and "range" for "seeAlso.
(I.e., "seeAlso" is a property whose arguments are resources.)
(PropertyValue domain seeAlso Resource) [seeAlso axiom 1]
(PropertyValue range seeAlso Resource) [seeAlso axiom 2]
4.2.4. isDefinedBy
%% "seeAlso" is a value of "subPropertyOf" for "isDefinedBy". (I.e.,
"isDefinedBy" is a subproperty of "seeAlso".)
(PropertyValue subPropertyOf isDefinedBy seeAlso) [isDefinedBy axiom 1]
4.2.5. comment
%% "Literal" is the value of "range" for "comment". (I.e., "comment" is
a property whose value is a literal.)
(PropertyValue range comment Literal) [comment axiom 1]
4.2.6. label
%% "Literal" is the value of "range" for "label". (I.e., "label" is a
property whose value is a literal.)
(PropertyValue range label Literal) [label axiom 1]
4.3. Constraint Properties
%% "Property" is a value of "subClassOf" for "ConstraintProperty".
(I.e., a constraint property is a property.)
(PropertyValue
subClassOf ConstraintProperty Property) [ConstraintProperty axiom 1]
4.3.1. range
%% "range" is type "ConstraintProperty" and "FunctionalProperty".
(Type range ConstraintProperty) [range axiom 1]
(FunctionalProperty range) [range axiom 2]
%% An object R is the value of "range" for an object P if and only if P
is type "Property", R is type "rdfs:Class", and if an object Y is a
value of P then Y is type R. (I.e., R is the range of P when P is a
property, R is a class, and every value of P is an R.)
(<=> (PropertyValue range ?p ?r)
(and (Type ?p Property)
(Type ?r rdfs:Class)
(forall (?x ?y) (=> (PropertyValue ?p ?x ?y)
(Type ?y ?r))))) [range axiom 3]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue range subClassOf rdfs:Class) [range theorem 1]
(PropertyValue range range rdfs:Class) [range theorem 2]
(PropertyValue range type rdfs:Class) [range theorem 3]
(PropertyValue range subject Resource) [range theorem 4]
(PropertyValue range predicate Property) [range theorem 5]
(PropertyValue range object Resource) [range theorem 6]
(PropertyValue range subPropertyOf Property) [range theorem 7]
(=> (and (PropertyValue range ?p ?r)
(PropertyValue ?p ?x ?y))
(Type ?y ?r)) [range theorem 8]
4.3.2. domain
%% "domain" is type "ConstraintProperty".
(Type domain ConstraintProperty) [domain axiom 1]
%% If an object D is a value of "domain" for an object P, then P is type
"Property", D is type "rdfs: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.)
(<=> (PropertyValue domain ?p ?d)
(and (Type ?p Property)
(Type ?d rdfs:Class)
(forall (?x ?y) (=> (PropertyValue ?p ?x ?y)
(Type ?x ?d))))) [domain axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue domain domain Property) [domain theorem 1]
(PropertyValue range domain rdfs:Class) [domain theorem 2]
(PropertyValue domain type Resource) [domain theorem 3]
(PropertyValue domain subject Statement) [domain theorem 4]
(PropertyValue domain predicate Statement) [domain theorem 5]
(PropertyValue domain object Statement) [domain theorem 6]
(PropertyValue domain subClassOf rdfs:Class) [domain theorem 7]
(PropertyValue domain range Property) [domain theorem 8]
(PropertyValue domain subPropertyOf Property) [domain theorem 9]
(=> (and (PropertyValue domain ?p ?d)
(PropertyValue ?p ?x ?y))
(Type ?x ?d)) [domain theorem 10]
(PropertyValue domain value Resource) [domain theorem 11]
%% For each positive integer i:
(PropertyValue domain _i Container) [domain theorem 11+i]
5. DAML+OIL
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.
The default namespace for the classes and properties defined in this section is
http://www.cs.man.ac.uk/~horrocks/daml+oil/datatypes/daml+oil+dt#.
5.1. Classes
This section axiomatizes the classes that are added to RDF and RDF-S.
5.1.1. Class
%% "Class" is a subclass of "rdfs:Class".
(PropertyValue subClassOf Class rdfs:Class) [class axiom 1]
5.1.2. Datatype
%% "Datatype" is a subclass of "rdfs:Class".
(PropertyValue subClassOf Datatype rdfs:Class) [Datatype axiom 1]
5.1.3. Thing
%% "Thing" is type "Class".
(Type Thing Class) [Thing axiom 1]
%% All objects X are type "Thing". (I.e., "Thing" is the class of all
objects.)
(Type ?x Thing) [Thing axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(=> (Type Class ?c)
(PropertyValue subClassOf ?c Thing)) [Thing theorem 1]
5.1.4. Nothing
%% "Nothing" is the value of "complementOf" for "Thing". (I.e.,
"Nothing" is the complement of "Thing".)
(PropertyValue complementOf Thing Nothing) [Nothing axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(=> (Type ?x Nothing) FALSE) [Nothing theorem 1]
5.1.5. Restriction
%% "Restriction" is a subclass of "Class".
(PropertyValue subClassOf Restriction Class) [Restriction axiom 1]
5.1.6. AbstractProperty
%% "AbstractProperty" is a subclass of "Property".
(PropertyValue
subClassOf AbstractProperty Property) [AbstractProperty axiom 1]
5.1.7. DatatypeProperty
%% "DatatypeProperty" is a subclass of "Class".
(PropertyValue
subClassOf DatatypeProperty Property) [DatatypeProperty axiom 1]
5.1.8. TransitiveProperty
%% An object P is type "TransitiveProperty" if and only if P is type
"AbstractProperty" and 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.
(<=> (Type ?p TransitiveProperty)
(and (Type ?p AbstractProperty)
(forall (?x ?y ?z)
(=> (and (PropertyValue ?p ?x ?y)
(PropertyValue ?p ?y ?z))
(PropertyValue
?p ?x ?z))))) [TransitiveProperty axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue subClassOf
TransitiveProperty
AbstractProperty) [TransitiveProperty theorem 1]
(Type subClassOf TransitiveProperty) [TransitiveProperty theorem 2]
(Type subPropertyOf TransitiveProperty) [TransitiveProperty theorem 3]
(=> (and (Type ?p TransitiveProperty)
(PropertyValue ?p ?x ?y)
(PropertyValue ?p ?y ?z))
(PropertyValue ?p ?x ?z)) [TransitiveProperty theorem 4]
5.1.9. UniqueProperty
%% An object P is type "UniqueProperty" if and only if P is type
"Property" and 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).
(<=> (Type ?p UniqueProperty)
(and (Type ?p Property)
(forall (?x ?y ?z) (=> (and (PropertyValue ?p ?x ?y)
(PropertyValue ?p ?x ?z))
(= ?y ?z))))) [UniqueProperty axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue
subClassOf UniqueProperty Property) [UniqueProperty theorem 1]
(Type predicate UniqueProperty) [UniqueProperty theorem 1]
(Type subject UniqueProperty) [UniqueProperty theorem 2]
(Type object UniqueProperty) [UniqueProperty theorem 3]
(Type range UniqueProperty) [UniqueProperty theorem 4]
%% For each positive integer i:
(Type _i UniqueProperty) [UniqueProperty theorem 6]
5.1.10. UnambiguousProperty
%% An object P is type "UnambiguousProperty" if and only if P is type
"AbstractProperty" and 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).
(<=> (Type ?p UnambiguousProperty)
(and (Type ?p AbstractProperty)
(forall (?x ?y ?v)
(=> (and (PropertyValue ?p ?x ?v)
(PropertyValue ?p ?y ?v))
(= ?x ?y))))) [UnambiguousProperty axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue subClassOf
UnambiguousProperty
AbstractProperty) [UnambiguousProperty theorem 1]
5.1.11. List
%% "Seq" is a value of "subClassOf" for "List". (I.e., lists are
sequences.)
(PropertyValue subClassOf List Seq) [List axiom 1]
5.1.12. Ontology
%% An ontology is type "Class".
(Type Ontology Class) [Ontology axiom 1]
5.2. Properties
This section axiomatizes the properties that are added to RDF and RDF-S.
5.2.1. equivalentTo
%% 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.)
(<=> (PropertyValue equivalentTo ?x ?y)
(= ?x ?y)) [equivalentTo axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue
inverseOf equivalentTo equivalentTo) [equivalentTo theorem 1]
(Type TransitiveProperty equivalentTo) [equivalentTo theorem 2]
(=> (Type ?x Thing)
(PropertyValue equivalentTo ?x ?x)) [equivalentTo theorem 3]
(=> (and (PropertyValue equivalentTo ?x ?y) (Type ?x ?c))
(Type ?y ?c)) [equivalentTo theorem 4]
(=> (and (Type ?p UniqueProperty)
(PropertyValue ?p ?x ?y)
(PropertyValue ?p ?x ?z))
(PropertyValue equivalentTo ?y ?z)) [equivalentTo theorem 5]
(=> (and (Type ?p UnambiguousProperty)
(PropertyValue ?p ?x ?v)
(PropertyValue ?p ?y ?v))
(PropertyValue equivalentTo ?x ?y)) [equivalentTo theorem 6]
5.2.2. sameClassAs
%% "equivalentTo" is a value of "subPropertyOf" for "sameClassAs".
(I.e., "sameClassAs" is "equivalentTo" for classes.)
(PropertyValue
subPropertyOf sameClassAs equivalentTo) [sameClassAs axiom 1]
%% C2 is a value of "sameClassAs" for C1 if and only if C2 is a value of
"subClassOf" for C1 and C1 is a value of "subClassOf" for C2.
(<=> (PropertyValue sameClassAs ?c1 ?c2)
(and (subClassOf ?c1 ?c2)
(subClassOf ?c2 ?c1))) [sameClassAs axiom 2]
%% If C1 is type "Class" and C2 is a value of "equivalentTo" for C1,
then C2 is a value of "sameClassAs" for C1 (i.e., if C1 is a class and
C1 is equivalent to C2, then C1 is sameClassAs C2).
(=> (and (Type ?c1 Class)
(PropertyValue equivalentTo ?c1 ?c2))
(PropertyValue sameClassAs ?c1 ?c2)) [sameClassAs axiom 3]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue
subPropertyOf sameClassAs subClassOf) [sameClassAs theorem 1]
(=> (and (PropertyValue subClassOf ?c1 ?c2)
(PropertyValue subClassOf ?c2 ?c1))
(PropertyValue sameClassAs ?c1 ?c2)) [sameClassAs theorem 2]
(=> (and (PropertyValue equivalentTo ?c1 ?c2)
(Type ?c1 Class))
(PropertyValue sameClassAs ?c1 ?c2)) [sameClassAs theorem 3]
5.2.3. samePropertyAs
%% "equivalentTo" is a value of "subPropertyOf" for "samePropertyAs".
(I.e., "samePropertyAs" is "equivalentTo" for properties.)
(PropertyValue
subPropertyOf samePropertyAs equivalentTo) [samePropertyAs axiom 1]
%% P2 is a value of "samePropertyAs" for P1 if and only if P2 is a value
of "subPropertyOf" for P1 and P1 is a value of "subPropertyOf" for P2.
(<=> (PropertyValue samePropertyAs ?P1 ?P2)
(and (subPropertyOf ?P1 ?P2)
(subPropertyOf ?P2 ?P1))) [samePropertyAs axiom 2]
%% If P1 is type "Property" and P2 is a value of "equivalentTo" for P1,
then P2 is a value of "samePropertyAs" for P1 (i.e., if P1 is a property
and P1 is equivalent to P2, then P1 is samePropertyAs P2).
(=> (and (Type ?P1 Property)
(PropertyValue equivalentTo ?P1 ?P2))
(PropertyValue samePropertyAs ?P1 ?P2)) [samePropertyAs axiom 3]
%% Note that the following can be inferred from the axioms regarding
"samePropertyAs" and "subPropertyOf":
(PropertyValue subPropertyOf
samePropertyAs
subPropertyOf) [samePropertyAs theorem 1]
(PropertyValue
inverseOf samePropertyAs samePropertyAs) [samePropertyAs theorem 2]
(=> (and (PropertyValue subPropertyOf ?p1 ?p2)
(PropertyValue subPropertyOf ?p2 ?p1))
(PropertyValue samePropertyAs ?p1 ?p2)) [samePropertyAs theorem 3]
(=> (and (PropertyValue equivalentTo ?p1 ?p2)
(Type ?p1 Property))
(PropertyValue samePropertyAs ?p1 ?p2)) [samePropertyAs theorem 4]
5.2.4. disjointWith
%% "disjointWith" is type "Property".
(Type disjointWith Property) [disjointWith axiom 1]
%% An object C2 is a value of "disjointWith" for an object C1 if and
only if C1 is type "Class", C2 is type "Class", and no object X is both
type C1 and type C2.
(<=> (PropertyValue disjointWith ?c1 ?c2)
(and (Type ?c1 Class)
(Type ?c2 Class)
(not (exists (?x)
(and (Type ?x ?c1)
(Type ?x ?c2)))))) [disjointWith axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue domain disjointWith Class) [disjointWith theorem 1]
(PropertyValue
inverseOf disjointWith disjointWith) [disjointWith theorem 2]
(PropertyValue disjointWith Property rdfs:Class) [disjointWith theorem 3]
(=> (and (PropertyValue disjointWith ?c1 ?c2)
(Type ?x ?c1)
(Type ?x ?c2))
FALSE) [disjointWith theorem 4]
(=> (and (PropertyValue disjointWith ?c1 ?c2)
(PropertyValue subClassOf ?c ?c1))
(PropertyValue disjointWith ?c ?c2)) [disjointWith theorem 5]
(=> (and (PropertyValue disjointWith ?c1 ?c2)
(PropertyValue subClassOf ?c ?c1)
(PropertyValue subClassOf ?c ?c2))
(PropertyValue sameClassAs ?c Nothing)) [disjointWith theorem 6]
5.2.5. unionOf
%% If an object L is a value of "unionOf" for an object C1, then 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.
(=> (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))))))) [unionOf axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue domain unionOf Class) [unionOf theorem 1]
(PropertyValue range unionOf List) [unionOf theorem 2]
(=> (and (PropertyValue unionOf ?c1 ?l)
(PropertyValue unionOf ?c2 ?l))
(PropertyValue sameClassAs ?c1 ?c2)) [unionOf theorem 3]
5.2.6. disjointUnionOf
%% An object L is a value of "disjointUnionOf" for an object C if and
only if L is a value of "unionOf" for C and L is "DisjointAll". (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.)
(<=> (PropertyValue disjointUnionOf ?c ?l)
(and (PropertyValue unionOf ?c ?l)
(DisjointAll ?l))) [disjointUnionOf axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue
subPropertyOf disjointUnionOf unionOf) [disjointUnionOf theorem 1]
5.2.7. intersectionOf
%% An object L is a value of "intersectionOf" for an object C1 if and
only if 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.
(<=> (PropertyValue intersectionOf ?c1 ?l)
(and (Type ?c1 Class)
(Type ?l List)
(forall (?c) (=> (PropertyValue item ?l ?c) (Type ?c Class)))
(forall (?x)
(<=> (Type ?x ?c1)
(forall
(?c2)
(=> (PropertyValue item ?l ?c2)
(Type
?x ?c2))))))) [intersectionOf axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue domain intersectionOf Class) [intersectionOf theorem 1]
(PropertyValue range intersectionOf List) [intersectionOf theorem 2]
5.2.8. complementOf
%% An object C2 is a value of "complementOf" for an object C1 if and
only if C1 and C2 are disjoint classes and all objects are either type
C1 or type C2.
(<=> (PropertyValue complementOf ?c1 ?c2)
(and (PropertyValue disjointWith ?c1 ?c2)
(forall (?x) (or (Type ?x ?c1)
(Type ?x ?c2))))) [complementOf axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue
subPropertyOf complementOf disjointWith) [complementOf theorem 1]
(PropertyValue
inverseOf complementOf complementOf) [complementOf theorem 2]
(=> (and (PropertyValue complementOf ?c1 ?c2)
(PropertyValue disjointWith ?c1 ?c3))
(PropertyValue subClassOf ?c3 ?c2)) [complementOf theorem 3]
(=> (and (PropertyValue complementOf ?c1 ?c2)
(PropertyValue complementOf ?c3 ?c4)
(PropertyValue subClassOf ?c1 ?c3))
(PropertyValue subClassOf ?c4 ?c2)) [complementOf theorem 4]
5.2.9. oneOf
%% An object L is a value of "oneOf" for an object C if and only if 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.)
(<=> (PropertyValue oneOf ?c ?l)
(and (Type ?c Class)
(Type ?l List)
(forall (?x)
(<=> (Type ?x ?c)
(PropertyValue item ?l ?x))))) [oneOf axiom 1]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue domain oneOf Class) [oneOf theorem 1]
(PropertyValue range oneOf List) [oneOf theorem 2]
(=> (and (PropertyValue oneOf ?c1 ?l)
(PropertyValue oneOf ?c2 ?l))
(PropertyValue sameClassAs ?c1 ?c2)) [oneOf theorem 3]
5.2.10. onProperty
%% "Restriction" is a value of "domain" for "onProperty". (I.e., the
first argument of onProperty is a restriction.)
(PropertyValue domain onProperty Restriction) [onProperty axiom 1]
%% "Property" is the value of "range" for "onProperty". (I.e., the
second argument of onProperty is a property.)
(PropertyValue range onProperty Property) [onProperty axiom 2]
5.2.11. toClass
%% "Restriction" is a value of "domain" for "toClass". (I.e., the first
argument of toClass is a restriction.)
(PropertyValue domain toClass Restriction) [toClass axiom 1]
%% "rdfs:Class" is the value of "range" for "toClass". (I.e., the
second argument of toClass is a class.)
(PropertyValue range toClass rdfs:Class) [toClass axiom 2]
%% 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.)
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue toClass ?r ?c))
(forall (?i) (<=> (Type ?i ?r)
(forall (?j)
(=> (PropertyValue ?p ?i ?j)
(Type ?j ?c)))))) [toClass axiom 3]
%% Note that the following can be inferred from the preceding axioms:
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue toClass ?r ?c)
(Type ?x ?r)
(PropertyValue ?p ?x ?v))
(Type ?v ?c)) [toClass theorem 1]
(=> (and (PropertyValue onProperty ?r1 ?p)
(PropertyValue toClass ?r1 ?c1)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue toClass ?r2 ?c2)
(PropertyValue subClassOf ?c1 ?c2))
(PropertyValue subClassOf ?r1 ?r2)) [toClass theorem 2]
(=> (and (PropertyValue onProperty ?r1 ?p)
(PropertyValue toClass ?r1 ?c1)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue toClass ?r2 ?c2)
(PropertyValue disjointWith ?c1 ?c2))
(PropertyValue disjointWith ?r1 ?r2)) [toClass theorem 3]
5.2.12. hasValue
%% "Restriction" is a value of "domain" for "hasValue". (I.e., the
first argument of hasValue is a restriction.)
(PropertyValue domain hasValue Restriction) [hasValue axiom 1]
%% 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.)
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue hasValue ?r ?v))
(forall (?i) (<=> (Type ?i ?r)
(PropertyValue ?p ?i ?v)))) [hasValue axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue hasValue ?r ?v)
(Type ?i ?r))
(PropertyValue ?p ?i ?v)) [hasValue theorem 1]
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue hasValue ?r ?v)
(PropertyValue ?p ?i ?v))
(Type ?i ?r)) [hasValue theorem 2]
5.2.13. hasClass
%% "Restriction" is a value of "domain" for "hasClass". (I.e., the
first argument of hasClass is a restriction.)
(PropertyValue domain hasClass Restriction) [hasClass axiom 1]
%% "rdfs:Class" is the value of "range" for "hasClass". (I.e., the
second argument of hasClass is a class.)
(PropertyValue range hasClass rdfs:Class) [hasClass axiom 2]
%% If a property P is a value of "onProperty" and a class C is a value
of "hasClass" for a restriction R, then R is a value of "Type" for an
object X if and only if there exists a V that is a value of P for X and
that has C as a value of "Type". (I.e., a "hasClass" restriction of C
on a property P is the class of all objects that have a value of P that
is type C.)
(=> (and (PropertyValue hasClass ?r ?c)
(PropertyValue onProperty ?r ?p))
(forall (?x)
(<=> (Type ?x ?r)
(exists (?v) (and (PropertyValue ?p ?x ?v)
(Type ?v ?c)))))) [hasClass axiom 3]
%% Note that the following can be inferred from the preceding axioms:
(=> (and (PropertyValue hasClass ?r ?c)
(PropertyValue onProperty ?r ?p)
(PropertyValue ?p ?x ?v)
(Type ?v ?c))
(Type ?x ?r)) [hasClass theorem 1]
5.2.14. minCardinality
%% "Restriction" is a value of "domain" for "minCardinality". (I.e.,
the first argument of minCardinality is a restriction.)
(PropertyValue
domain minCardinality Restriction) [minCardinality axiom 1]
%% "NonNegativeInteger" is the value of "range" for "minCardinality".
(I.e., the second argument of minCardinality is a non-negative integer.)
(PropertyValue
range minCardinality NonNegativeInteger) [minCardinality axiom 2]
%% 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 "NoRepeatsTuple" all of
whose items are values of P for I and whose length is greater than or
equal to N. (I.e., a "minCardinality" restriction of N on a property P
is the class of all objects I which have at least N values of P.)
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue minCardinality ?r ?n))
(forall (?i)
(<=> (Type ?i ?r)
(exists (?vl)
(and (NoRepeatsTuple ?vl)
(forall (?v)
(=> (Item ?vl ?v)
(PropertyValue ?p ?i ?v)))
(Length ?v1 ?l)
(>= ?l ?n)))))) [minCardinality axiom 3]
5.2.15. maxCardinality
%% "Restriction" is a value of "domain" for "maxCardinality". (I.e.,
the first argument of maxCardinality is a restriction.)
(PropertyValue
domain maxCardinality Restriction) [maxCardinality axiom 1]
%% "NonNegativeInteger" is the value of "range" for "maxCardinality".
(I.e., the second argument of maxCardinality is a non-negative integer.)
(PropertyValue
range maxCardinality NonNegativeInteger) [maxCardinality axiom 2]
%% If a property P is a value of "onProperty" for a restriction R and a
non-negative integer N is a value of "maxCardinality" for R, then an
object I is type R if and only if all "NoRepeatsTuples" whose items are
exactly the values of P have length less than or equal to N. (I.e., a
"maxCardinality" restriction of N on a property P is the class of all
objects I which have at most N values of P.)
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue maxCardinality ?r ?n))
(forall (?i)
(<=> (Type ?i ?r)
(forall (?vl)
(=> (and (NoRepeatsTuple ?vl)
(forall (?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?i ?v))))
(=< (length ?vl)
?n)))))) [maxCardinality axiom 3]
5.2.16. cardinality
%% "Restriction" is a value of "domain" for "cardinality". (I.e., the
first argument of cardinality is a restriction.)
(PropertyValue domain cardinality Restriction) [cardinality axiom 1]
%% "NonNegativeInteger" is the value of "range" for "cardinality".
(I.e., the second argument of cardinality is a non-negative integer.)
(PropertyValue
range cardinality NonNegativeInteger) [cardinality axiom 2]
%% If a property P is a value of "onProperty" for a restriction R and a
non-negative integer N is a value of "cardinality" for R, then an object
I is type R if and only if all "NoRepeatsTuples" whose items are exactly
the values of P have length N. (I.e., a "cardinality" restriction of N
on a property P is the class of all objects I which have exactly N
values of P.)
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue cardinality ?r ?n))
(forall (?i) (<=> (Type ?i ?r)
(forall (?vl)
(=> (and (NoRepeatsTuple ?vl)
(forall
(?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?i ?v))))
(= (length ?vl)
?n)))))) [cardinality axiom 3]
5.2.17. hasClassQ
%% "Restriction" is a value of "domain" for "hasClassQ". (I.e., the
first argument of hasClassQ is a restriction.)
(PropertyValue domain hasClassQ Restriction) [hasClassQ axiom 1]
%% "rdfs:Class" is the value of "range" for "hasClassQ". (I.e., the
second argument of hasClassQ is a class.)
(PropertyValue range hasClassQ rdfs:Class) [hasClassQ axiom 2]
5.2.18. minCardinalityQ
%% "Restriction" is a value of "domain" for "minCardinalityQ". (I.e.,
the first argument of minCardinalityQ is a restriction.)
(PropertyValue
domain minCardinalityQ Restriction) [minCardinalityQ axiom 1]
%% "NonNegativeInteger" is the value of "range" for "minCardinalityQ".
(I.e., the second argument of minCardinalityQ is a non-negative
integer.)
(PropertyValue
range minCardinalityQ NonNegativeInteger) [minCardinalityQ axiom 2]
%% If a property P is a value of "onProperty" for a restriction R, a
non-negative integer N is a value of "minCardinalityQ" for R, and a
class C is a value of "hasClassQ" for R, then an object I is type R if
and only if there is a "NoRepeatsTuple" all of whose items are type C
and values of P for I and whose length is greater than or equal to N.
(I.e., a "minCardinalityQ" restriction of N on a property P is the class
of all objects I which have at least N values of P that are type C.)
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue minCardinalityQ ?r ?n)
(PropertyValue hasClassQ ?r ?c))
(forall (?i)
(<=> (Type ?i ?r)
(exists
(?vl)
(and (NoRepeatsTuple ?vl)
(forall (?v) (=> (PropertyValue item ?vl ?v)
(and (PropertyValue ?p ?i ?v)
(Type ?v ?c)))
(>= (length ?vl)
?n)))))) [minCardinalityQ axiom 3]
%% Note that the following can be inferred from the preceding axioms:
(=> (and (PropertyValue minCardinality ?r1 ?n)
(PropertyValue onProperty ?r1 ?p)
(PropertyValue minCardinalityQ ?r2 ?n)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue hasClassQ ?r2 Thing))
(PropertyValue sameClassAs ?r1 ?r2)) [minCardinalityQ theorem 1]
(=> (and (PropertyValue hasValue ?r1 ?v)
(PropertyValue onProperty ?r1 ?p)
(Type ?v ?c)
(PropertyValue hasClassQ ?r2 ?c)
(PropertyValue minCardinalityQ ?r2 1)
(PropertyValue onProperty ?r1 ?p))
(PropertyValue subClassOf ?r1 ?r2)) [minCardinalityQ theorem 2]
(=> (and (PropertyValue hasClass ?r1 ?c)
(PropertyValue onProperty ?r1 ?p)
(PropertyValue hasClassQ ?r2 ?c)
(PropertyValue minCardinalityQ ?r2 1))
(PropertyValue sameClassAs ?r2 ?r1)) [minCardinalityQ theorem 3]
(=> (and (PropertyValue minCardinalityQ ?r1 ?n1)
(PropertyValue onProperty ?r1 ?p)
(PropertyValue hasClassQ ?r1 ?c1)
(PropertyValue minCardinalityQ ?r2 ?n2)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue hasClassQ ?r2 ?c2)
(PropertyValue subClassOf ?c1 ?c2)
(>= ?n1 ?n2))
(PropertyValue subClassOf ?r1 ?r2)) [minCardinalityQ theorem 4]
5.2.19. maxCardinalityQ
%% "Restriction" is a value of "domain" for "maxCardinalityQ". (I.e.,
the first argument of maxCardinalityQ is a restriction.)
(PropertyValue
domain maxCardinalityQ Restriction) [maxCardinalityQ axiom 1]
%% "NonNegativeInteger" is the value of "range" for "maxCardinalityQ".
(I.e., the second argument of maxCardinalityQ is a non-negative
integer.)
(PropertyValue
range maxCardinalityQ NonNegativeInteger) [maxCardinalityQ axiom 2]
%% If a property P is a value of "onProperty" for a restriction R, a
non-negative integer N is a value of "maxCardinalityQ" for R, and a
class C is a value of "hasClassQ" for R, then an object I is type R if
and only if all "NoRepeatsTuples" whose items are exactly the values of
P that are type C have length less than or equal to N. (I.e., a
"maxCardinalityQ" restriction of N on a property P is the class of all
objects I which have at most N values of P that are type C.)
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue maxCardinalityQ ?r ?n)
(PropertyValue hasClassQ ?r ?c))
(forall (?i) (<=> (Type ?i ?r)
(forall
(?vl)
(=> (and (NoRepeatsTuple ?vl)
(forall
(?v)
(<=> (PropertyValue item ?vl ?v)
(and (PropertyValue ?p ?i ?v)
(Type ?v ?c)))))
(=< (length ?vl)
?n)))))) [maxCardinalityQ axiom 3]
%% Note that the following can be inferred from the preceding axioms:
(=> (and (PropertyValue maxCardinality ?r1 ?n)
(PropertyValue onProperty ?r1 ?p)
(PropertyValue maxCardinalityQ ?r2 ?n)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue hasClassQ ?r2 Thing))
(PropertyValue sameClassAs ?r1 ?r2)) [maxCardinalityQ theorem 1]
(=> (and (PropertyValue minCardinalityQ ?r1 ?n1)
(PropertyValue onProperty ?r1 ?p)
(PropertyValue hasClassQ ?r1 ?c1)
(PropertyValue maxCardinalityQ ?r2 ?n2)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue hasClassQ ?r2 ?c2)
(PropertyValue subClassOf ?c1 ?c2)
(> ?n1 ?n2))
(PropertyValue disjointWith ?r1 ?r2)) [maxCardinalityQ theorem 2]
(=> (and (PropertyValue maxCardinalityQ ?r 0)
(PropertyValue onProperty ?r ?p)
(PropertyValue hasClassQ ?r ?c)
(Type ?x ?r)
(PropertyValue ?p ?x ?v)
(Type ?v ?c))
FALSE) [maxCardinalityQ theorem 3]
(=> (and (PropertyValue maxCardinalityQ ?r 1)
(PropertyValue onProperty ?r ?p)
(PropertyValue hasClassQ ?r ?c)
(Type ?x ?r)
(PropertyValue ?p ?x ?v1)
(Type ?v1 ?c)
(PropertyValue ?p ?x ?v2)
(Type ?v2 ?c))
(PropertyValue equivalentTo ?v1 ?v2)) [maxCardinalityQ theorem 4]
(=> (and (PropertyValue maxCardinalityQ ?r1 ?n1)
(PropertyValue onProperty ?r1 ?p)
(PropertyValue hasClassQ ?r1 ?c1)
(PropertyValue maxCardinalityQ ?r2 ?n2)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue hasClassQ ?r2 ?c2)
(PropertyValue subClassOf ?c2 ?c1)
(< ?n1 ?n2))
(PropertyValue subClassOf ?r1 ?r2)) [maxCardinalityQ theorem 5]
5.2.20. cardinalityQ
%% "Restriction" is a value of "domain" for "cardinalityQ". (I.e., the
first argument of cardinalityQ is a restriction.)
(PropertyValue domain cardinalityQ Restriction) [cardinalityQ axiom 1]
%% "NonNegativeInteger" is the value of "range" for "cardinalityQ".
(I.e., the second argument of cardinalityQ is a non-negative integer.)
(PropertyValue
range cardinalityQ NonNegativeInteger) [cardinalityQ axiom 2]
%% If a property P is a value of "onProperty" for a restriction R, a
non-negative integer N is a value of "cardinalityQ" for R and a class C
is a value of "hasClassQ" for R, then an object I is type R if and only
if all "NoRepeatsTuples" whose items are exactly the values of P that
are type C have length N. (I.e., a "cardinalityQ" restriction of N on a
property P is the class of all objects I which have exactly N values of
P that are type C.)
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue cardinalityQ ?r ?n)
(PropertyValue hasClassQ ?r ?c))
(forall (?i) (<=> (Type ?i ?r)
(forall
(?vl)
(=> (and (NoRepeatsTuple ?vl)
(forall
(?v)
(<=> (PropertyValue item ?vl ?v)
(and (PropertyValue ?p ?i ?v)
(Type ?v ?c)))))
(= (length ?vl)
?n)))))) [cardinalityQ axiom 4]
%% Note that the following can be inferred from the preceding axioms:
(=> (and (PropertyValue cardinality ?r1 ?n)
(PropertyValue onProperty ?r1 ?p)
(PropertyValue cardinalityQ ?r2 ?n)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue hasClassQ ?r2 Thing))
(PropertyValue sameClassAs ?r1 ?r2)) [cardinalityQ theorem 1]
(=> (and (PropertyValue cardinalityQ ?r1 ?n)
(PropertyValue onProperty ?r1 ?p)
(PropertyValue hasClassQ ?r1 ?c)
(PropertyValue minCardinalityQ ?r2 ?n)
(PropertyValue onProperty ?r2 ?p)
(PropertyValue hasClassQ ?r2 ?c)
(PropertyValue maxCardinalityQ ?r3 ?n)
(PropertyValue onProperty ?r3 ?p)
(PropertyValue hasClassQ ?r3 ?c)
(PropertyValue first ?l1 ?r2)
(PropertyValue rest ?l1 ?l2)
(PropertyValue first ?l2 ?r3)
(PropertyValue rest ?l2 nil))
(PropertyValue intersectionOf ?r1 ?l1)) [cardinalityQ theorem 2]
5.2.21. inverseOf
%% "inverseOf" is type "Property".
(Type inverseOf Property) [inverseOf axiom 1]
%% An object P2 is a value of "inverseOf" for an object P1 if and only
if P1 is type "AbstractProperty", P2 is type "AbstractProperty", and an
object X2 is a value of P1 for an object X1 if and only X1 is a value of
P2 for X2.
(<=> (PropertyValue inverseOf ?p1 ?p2)
(and (Type ?p1 AbstractProperty)
(Type ?p2 AbstractProperty)
(forall (?x1 ?x2)
(<=> (PropertyValue ?p1 ?x1 ?x2)
(PropertyValue
?p2 ?x2 ?x1))))) [inverseOf axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue domain inverseOf AbstractProperty) [inverseOf theorem 1]
(PropertyValue range inverseOf AbstractProperty) [inverseOf theorem 2]
(=> (and (PropertyValue inverseOf ?p1 ?p2)
(PropertyValue ?p1 ?x1 ?x2))
(PropertyValue ?p2 ?x2 ?x1)) [inverseOf theorem 3]
5.2.22. first
%% "first" is type "UniqueProperty".
(Type first UniqueProperty) [first axiom 1]
%% An object X is the value of "first" for an object L if and only if L
is type "List" and the value of "_1" for L is X. (I.e., "first" is "_1"
for lists.)
(<=> (PropertyValue first ?l ?x)
(and (Type ?l List) (PropertyValue _1 ?l ?x))) [first axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue domain first List) [first theorem 1]
(PropertyValue subPropertyOf first _1) [first theorem 2]
(=> (and (Type ?l List) (PropertyValue _1 ?l ?x))
(PropertyValue first ?l ?x)) [first theorem 3]
5.2.23. rest
%% "rest" is type "UniqueProperty".
(Type rest UniqueProperty) [rest axiom 1]
%% An object R is the value of "rest" for an object L if and only if L
is type "List", R is type "List", and L has the same items in the same
order as list R with one additional object as its first item.
(<=> (PropertyValue rest ?l ?r)
(and (Type ?l List)
(Type ?r List)
(exists (?x) (= ?l (cons ?x ?r))))) [rest axiom 2]
%% Note that the following can be inferred given the axioms regarding
"rest":
(PropertyValue domain rest List) [rest theorem 1]
(PropertyValue range rest List) [rest theorem 2]
(Type rest uniqueProperty) [rest theorem 3]
%% For each positive integer N, the following can be inferred:
(=> (and (PropertyValue rest ?l ?r)
(PropertyValue _N ?r ?x))
(PropertyValue _N+1 ?l ?x)) [rest theorem 3+N]
5.2.24. item
%% "item" is type "Property".
(Type item Property) [item axiom 1]
%% An object X is a value of "item" for an object L if and only if L is
type "List" and either X is the value of "first" for L or X is a value
of "item" for the value of "rest" of L. (I.e., Saying that X is an item
of L is saying that 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.)
(<=> (PropertyValue item ?l ?x)
(and (Type ?l List)
(or (PropertyValue first ?l ?x)
(exists (?r)
(and (PropertyValue rest ?l ?r)
(PropertyValue
item ?r ?x)))))) [item axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(PropertyValue domain item List) [item theorem 1]
(=> (and (PropertyValue unionOf ?c ?l)
(PropertyValue item ?l ?c1))
(PropertyValue subClassOf ?c1 ?c)) [item theorem 2]
(=> (and (PropertyValue intersectionOf ?c ?l)
(PropertyValue item ?l ?c1))
(PropertyValue subClassOf ?c ?c1)) [item theorem 3]
(=> (and (PropertyValue oneOf ?c ?l)
(Type ?x ?c))
(PropertyValue item ?l ?x)) [item theorem 4]
(=> (and (PropertyValue oneOf ?c ?l)
(PropertyValue item ?l ?x))
(Type ?x ?c)) [item theorem 5]
(=> (and (PropertyValue rest ?l ?r)
(PropertyValue item ?r ?x))
(PropertyValue item ?l ?x)) [item theorem 6]
(PropertyValue subPropertyOf first item) [item theorem 7]
%% For each positive integer N, the following can be inferred:
(=> (and (Type ?l List)
(PropertyValue _N ?l ?x))
(PropertyValue item ?l ?x)) [item theorem 7+N]
5.2.25. versionInfo
%% "versionInfo" is a property.
(Type versionInfo Property) [versionInfo axiom 1]
5.2.26. imports
%% "imports" is a property.
(Type imports Property) [imports axiom 1]
5.3. Other Objects
5.3.1. nil
%% "nil" is a list for which there are no values of "item". (I.e.,
"nil" is the empty list.)
(Type nil List) [nil axiom 1]
(not (PropertyValue item nil ?x)) [nil axiom 2]
%% Note that the following can be inferred from the preceding axioms:
(=> (PropertyValue first nil ?x) FALSE) [nil theorem 1]
(=> (PropertyValue rest nil ?x) FALSE) [nil theorem 2]
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, Peter Patel-Schneider, and Richard Waldinger for their
generous help in debugging earlier versions of this document. We would also like to acknowledge
constructive comments from many on the RDF mailing list including Ken Baclawski, Alex Borgida, Dan
Connolly, and Ora Lassila.
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 note: "=>" means "implies".
We do not use the properties "domain" and "range" in the RDF axioms since those properties are defined
in RDF-S.
We do not use the property "subClassOf" in the RDF axioms since "subClassOf" is a property defined in
RDF-S.
KIF note: ">=" is the KIF relation for "greater than or equal".
KIF note: "=<" is the KIF relation for "less than or equal".
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.