An Axiomatic Semantics for RDF, RDF-S, and DAML+OIL
Richard Fikes
Deborah L McGuinness
Knowledge Systems Laboratory
Computer Science Department
July 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/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.[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.
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.
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”.
%% 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[3]
?s ?o))[4] [Type axiom 1]
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) [FunctionalProperty axiom 1]
(and (Type ?fp Property)
(forall (?s ?v1 ?v2)
(=> (and (PropertyValue
?fp ?s ?v1)
(PropertyValue ?fp
?s ?v2))
(= ?v1 ?v2))))
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) [DisjointAll axiom
1]
(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)))))))
The relation NoRepeatsList is used in the axiomatization of DAML+OIL properties “cardinality”, “minCardinality”, and “maxCardinality”.
%% A
“NoRepeatsList” is a list for which no item occurs more than once.
(<=> (NoRepeatsList ?l) [NoRepeatsList axiom
1]
(or (= ?l nil)
(exists (?x) (= ?l (listof ?x)))
(and (not (item (rest ?l) (first ?l)))
(NoRepeatsList (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)”.
The default namespace for the classes and properties defined in this section is http://www.w3.org/1999/02/22-rdf-syntax-ns#.
This section axiomatizes the classes that are included in RDF.
All things being described by RDF expressions are called resources.
%% “Resource” is
type “rdfs:Class”.
(Type Resource rdfs:Class) [Resource axiom 1]
%% The first
argument of relation “PropertyValue” is type “Property”.
(=> (PropertyValue ?p ?s ?o) (Type ?p
Property))[6] [Property
axiom 1]
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]
%% “Literal” is
type “rdfs:Class”.
(Type Literal rdfs:Class) [Literal axiom 1]
%% 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) [Statement axiom 1]
(exists (?p ?r ?o) (and (PropertyValue
predicate ?st ?p)
(PropertyValue
subject ?st ?r)
(PropertyValue
object ?st ?o))))
%% 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) [Container axiom 2]
(or (Type ?c Bag) (Type ?c Seq) (Type ?c
Alt)))
%% If an object C
is type “ContainerMembershipProperty”, then C is also type “Property”. (I.e., container membership properties are
properties.)
(=> (Type ?c [ContainerMembershipProperty axiom 1]
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.)
(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) [type axiom 2]
(and (Type ?r Resource) (Type
?c rdfs:Class)))[7]
%% Note that the
following can be inferred from the axioms regarding “type”:
(=> (Type ?p Property) (Type ?p
Resource))[8] [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]
%% “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) [subject axiom 2]
(and (Type ?st Statement) (Type ?sb
Resource)))
%% “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) [predicate axiom 2]
(and (Type ?st Statement) (Type ?p
Property)))
%% “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) [object axiom 2]
(and (Type ?st Statement) (Type ?o
Resource)))
%% “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) [value axiom 2]
(and (Type ?sv Resource) (Type ?v
Resource)))
%% 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.
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#.
This section axiomatizes the classes that are added to RDF in RDF-S.
%% “Resource” is a
value of “subClassOf” for “ConstraintResource”.
(I.e., constraint resources are resources.)
(PropertyValue [ConstraintResource axiom 1]
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.)
(<=> (Type ?cp ConstraintProperty) [ConstraintProperty axiom 1]
(and (Type ?cp ConstraintResource) (Type
?cp Property)))
%% An object of
type “NonNegativeInteger” is an integer.
(=> (Type ?n NonNegativeInteger) [NonNegativeInteger
axiom 1]
(Integer
?n))
This section axiomatizes the properties that are added to RDF in RDF-S.
%% “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) [subClassOf axiom 2]
(and (Type ?csub rdfs:Class)
(Type ?csuper rdfs:Class)
(forall (?x) (=> (Type ?x ?csub)
(Type ?x ?csuper)))))
%% Note that the
following can be inferred from the axioms regarding “subClassOf”, “domain”,
“range”, “Property”, “rdfs:Class”, “Statement”, “Resource”, “Bag”, “Seq”,
“Alt”, “Container”, and “ContainerMembershipProperty”:
(PropertyValue domain subClassOf
rdfs:Class) [subClassOf theorem 1]
(PropertyValue range subClassOf rdfs:Class) [subClassOf theorem 2]
(PropertyValue subClassOf Property
Resource) [subClassOf theorem 3]
(PropertyValue subClassOf rdfs:Class
Resource) [subClassOf theorem 4]
(PropertyValue subClassOf Statement
Resource) [subClassOf theorem 5]
(PropertyValue subClassOf Bag Container) [subClassOf theorem 6]
(PropertyValue subClassOf Seq Container) [subClassOf theorem 7]
(PropertyValue subClassOf Alt Container) [subClassOf theorem 8]
(PropertyValue [subClassOf theorem 9]
subClassOf ContainerMembershipProperty
Property)
%% 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) [subPropertyOf axiom 1]
(and (Type ?subP Property)
(Type ?superP Property)
(forall (?o ?v) (=> (PropertyValue
?subP ?o ?v)
(PropertyValue
?superP ?o ?v)))))
%% Note that the
following can be inferred from the axioms regarding “subPropertyOf”, “domain”,
and “range”:
(PropertyValue domain subPropertyOf
Property) [subPropertyOf theorem 1]
(PropertyValue range subPropertyOf
Property) [subPropertyOf theorem 2]
%% “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]
%% “seeAlso” is a
value of “subPropertyOf” for “isDefinedBy”.
(I.e., “isDefinedBy” is a subproperty of “seeAlso”.)
(PropertyValue subPropertyOf isDefinedBy
seeAlso) [isDefinedBy axiom 1]
%% “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]
%% “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]
%% “Property” is a
value of “subClassOf” for “ConstraintProperty”.
(I.e., constraint properties are properties.)
(PropertyValue [ConstraintProperty axiom 1]
subClassOf ConstraintProperty
Property)
%% “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) [range axiom 3]
(and (Type ?p Property)
(Type ?r rdfs:Class)
(forall (?x ?y) (=> (PropertyValue
?p ?x ?y) (Type ?y ?r)))))
%% Note that the
following can be inferred from the axioms regarding “domain”, “range”, “type”,
“subject”, and “predicate”:
(PropertyValue domain range Property) [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]
%% “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) [domain axiom 2]
(and (Type ?p Property)
(Type ?d rdfs:Class)
(forall (?x ?y) (=> (PropertyValue
?p ?x ?y) (Type ?x ?d)))))
%% Note that the
following can be inferred from the axioms regarding “domain”, “range”, “type”,
“subject”, “predicate”, and “object”:
(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]
%% For each
positive integer i:
(PropertyValue domain _i Container) [domain theorem 6+i]
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#.
This section axiomatizes the classes that are added to RDF and RDF-S.
%% “Class” is a
subclass of “rdfs:Class”.
(PropertyValue subClassOf Class rdfs:Class) [class axiom 1]
%% “Datatype” is a
subclass of “rdfs:Class”.
(PropertyValue subClassOf Datatype
rdfs:Class) [Datatype axiom 1]
%% “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]
%% “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 axioms regarding “Thing” and “complementOf”:
(not (Type ?x Nothing)) [Nothing theorem
1]
%% “Restriction”
is a subclass of “Class”.
(PropertyValue subClassOf Restriction
Class) [Restriction axiom 1]
%% “Restriction”
is a subclass of “Class”.
(PropertyValue [AbstractProperty axiom 1]
subClassOf AbstractProperty
Property)
%% “Restriction”
is a subclass of “Class”.
(PropertyValue [DatatypeProperty axiom 1]
subClassOf DatatypeProperty
Class)
%% 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) [TransitiveProperty axiom 1]
(and (Type ?p AbstractProperty)
(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”,
“subClassOf”, and “subPropertyOf”:
(PropertyValue [TransitiveProperty theorem 1]
subClassOf TransitiveProperty
AbstractProperty)
(Type subClassOf TransitiveProperty) [TransitiveProperty theorem 2]
(Type subPropertyOf TransitiveProperty) [TransitiveProperty theorem 3]
%% 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) [UniqueProperty axiom 1]
(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”,
“subClassOf”, “predicate”, “subject”, “object”, and “range”:
(PropertyValue [UniqueProperty theorem 1]
subClassOf UniqueProperty
Property)
(Type predicate UniqueProperty) [UniqueProperty theorem 1]
(Type subject UniqueProperty) [UniqueProperty theorem 2]
(Type object UniqueProperty) [UniqueProperty theorem 3]
(Type range UniqueProperty) [UniqueProperty theorem 4]
(=> (Type ?p UniqueProperty) [UniqueProperty theorem 5]
(=> (PropertyValue onProperty ?r ?p)
(PropertyValue cardinality ?r 1)))
%% For each
positive integer i:
(Type _i UniqueProperty) [UniqueProperty theorem 6]
%% 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) [UnambiguousProperty axiom 1]
(and (Type ?p AbstractProperty)
(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”:
(PropertyValue [UnambiguousProperty theorem 1]
subClassOf UnambiguousProperty
AbstractProperty)
%% “Seq” is a
value of “subClassOf” for “List”. (I.e.,
lists are sequences.)
(PropertyValue subClassOf List Seq) [List axiom 1]
%% An ontology is
type “Class”.
(Type Ontology Class) [Ontology axiom
1]
This section axiomatizes the properties that are added to RDF and RDF-S.
%% 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) [equivalentTo axiom 1]
(= ?x ?y))
%% “equivalentTo”
is its own inverse (i.e., it is symmetric).
(PropertyValue [equivalentTo axiom 2]
inverseOf equivalentTo
equivalentTo)
%% “equivalentTo”
is a value of “subPropertyOf” for “sameClassAs”. (I.e., “sameClassAs” is “equivalentTo” for
classes.)
(PropertyValue [sameClassAs axiom 1]
subPropertyOf sameClassAs
equivalentTo)
%% “sameClassAs”
is its own inverse (i.e., it is symmetric).
(PropertyValue inverseOf sameClassAs
sameClassAs) [sameClassAs axiom 2]
%% 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) [sameClassAs axiom 3]
(and (subClassOf ?c1 ?c2) (subClassOf ?c2
?c1)))
%% Note that the
following can be inferred from the axioms regarding “sameClassAs” and “subPropertyOf”:
(PropertyValue [sameClassAs theorem 1]
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.)
(PropertyValue [samePropertyAs axiom 1]
subPropertyOf samePropertyAs
equivalentTo)
(PropertyValue [samePropertyAs axiom 2]
subPropertyOf samePropertyAs
subPropertyOf)
%% “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) [disjointWith axiom 2]
(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”,
“range”, “Property”, “rdfs:Class”, and “subClassOf”:
(PropertyValue domain disjointWith Class) [disjointWith theorem 1]
(PropertyValue range disjointWith Class) [disjointWith theorem 2]
(PropertyValue [disjointWith theorem 3]
inverseOf disjointWith
disjointWith)
(PropertyValue disjointWith Property
rdfs:Class) [disjointWith theorem 4]
(=> (PropertyValue disjointWith ?c1 ?c2) [disjointWith theorem 5]
(=> (PropertyValue subClassOf ?c ?c1)
(PropertyValue disjointWith ?c ?c2)))
%% 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) [unionOf axiom 1]
(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”,
“range”, “sameClassAs”, and “subClassOf”:
(PropertyValue domain unionOf Class) [unionOf theorem 1]
(PropertyValue range unionOf List) [unionOf theorem 1]
(=> (PropertyValue unionOf ?c ?l) [unionOf theorem 1]
(=> (PropertyValue item ?l ?c1)
(PropertyValue subClassOf ?c1 ?c)))
(=> (and (PropertyValue unionOf ?c1 ?l) [unionOf theorem 1]
(PropertyValue unionOf ?c2 ?l))
(PropertyValue sameClassAs ?c1 ?c2))
%% 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) [disjointUnionOf axiom 1]
(and (PropertyValue unionOf ?c ?l)
(DisjointAll ?l)))
%% Note that the
following can be inferred from the axioms regarding “disjointUnionOf”,
“unionOf”, “domain”, and “range”:
(PropertyValue domain disjointUnionOf
Class) [disjointUnionOf theorem 1]
(PropertyValue [disjointUnionOf theorem 1]
range disjointUnionOf
Disjoint)
(PropertyValue [disjointUnionOf theorem 1]
subPropertyOf disjointUnionOf
unionOf)
%% 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) [intersectionOf axiom 1]
(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 )))))))
%% Note that the
following can be inferred from the axioms regarding “intersectionOf”, “domain”,
“range”, and “ConstraintProperty”:
(PropertyValue domain intersectionOf Class) [intersectionOf theorem 1]
(PropertyValue range intersectionOf List) [intersectionOf theorem 2]
(=> (PropertyValue intersectionOf ?c ?l) [intersectionOf theorem 3]
(=> (PropertyValue item ?l ?c1)
(PropertyValue subClassOf ?c ?c1)))
(exists (?l ?r) [intersectionOf theorem 4]
(and (PropertyValue first ?l
ConstraintResource)
(PropertyValue rest ?l ?r)
(PropertyValue first ?r Property)
(PropertyValue rest ?r nil)
(PropertyValue intersectionOf ConstraintProperty ?l)))
%% 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) [complementOf axiom 1]
(and (PropertyValue disjointWith ?c1 ?c2)
(forall (?x) (or (Type ?x ?c1) (Type
?x ?c2)))))
%% 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) [complementOf axiom 2]
%% Note that the
following can be inferred from the axioms regarding “complementOf”,
“disjointWith”, “domain”, “range”, and “subClassOf”:
(PropertyValue [complementOf theorem 1]
subPropertyOf complementOf
disjointWith)
(PropertyValue [complementOf theorem 2]
inverseOf complementOf
complementOf)
(PropertyValue domain complementOf Class) [complementOf theorem 3]
(PropertyValue range complementOf Class) [complementOf theorem 4]
(=> (PropertyValue complementOf ?c1 ?c2) [complementOf theorem 5]
(=> (PropertyValue disjointWith ?c1 ?c3)
(PropertyValue subClassOf ?c2 ?c3)))
(PropertyValue complementOf Thing Nothing) [complementOf theorem 6]
%% 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) [oneOf axiom 1]
(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”:
(PropertyValue domain oneOf Class) [oneOf theorem 1]
(PropertyValue range oneOf List) [oneOf theorem 2]
(=> (and (PropertyValue oneOf ?c1 ?l) [oneOf theorem 3]
(PropertyValue oneOf ?c2 ?l))
(PropertyValue sameClassAs ?c1 ?c2))
%% “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]
%% “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) [toClass axiom 3]
(PropertyValue toClass ?r ?c))
(forall (?i) (<=> (Type ?i ?r)
(forall (?j) (=> (PropertyValue
?p ?i ?j)
(Type ?j
?c))))))
%% “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) [hasValue axiom 2]
(PropertyValue hasValue ?r ?v))
(forall (?i) (<=> (Type ?i ?r)
(PropertyValue ?p ?i ?v))))
%% “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” for a restriction R, then a class C is a value of
“hasClass” for R if and only if C is a value of “hasClassQ” for R and 1 is a
value of “minCardinalityQ” for R. (I.e.,
a “hasClass” restriction of C on a property P is equivalent to a
minCardinalityQ restriction of 1 to C on P.)
(<=> (PropertyValue hasClass ?r ?c) [hasClass axiom 3]
(and (PropertyValue hasClassQ ?r ?c)
(PropertyValue minCardinalityQ ?r
1)))
%% Note that the
following can be inferred from the axioms regarding “hasClass” and
“subPropertyOf”:
(PropertyValue subPropertyOf hasClass
hasClassQ) [hasClass theorem 1]
%% “Restriction”
is a value of “domain” for “minCardinality”.
(I.e., the first argument of minCardinality is a restriction.)
(PropertyValue [minCardinality axiom 1]
domain minCardinality
Restriction)
%%
“NonNegativeInteger” is the value of “range” for “minCardinality”. (I.e., the second argument of minCardinality
is a non-negative integer.)
(PropertyValue [minCardinality axiom 2]
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 “NoRepeatsList” 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) [minCardinality axiom 3]
(PropertyValue minCardinality ?r ?n))
(forall (?i) (<=> (Type ?i ?r)
(exists (?vl)
(and
(NoRepeatsList ?vl)
(forall (?v)
(=>
(PropertyValue item ?vl ?v)
(PropertyValue ?p ?i ?v)))
(>= (length ?vl)
?n))))))[9]
%% Note that the
following can be inferred from the axioms regarding “minCardinality”,
“maxCardinality”, and “cardinality”:
(=> (and (PropertyValue minCardinality
?r ?n) [minCardinality theorem 1]
(PropertyValue maxCardinality ?r ?x))
(=< ?n ?x))
(<=> (PropertyValue cardinality ?r
?n) [minCardinality theorem 2]
(and (PropertyValue minCardinality ?r ?n)
(PropertyValue maxCardinality ?r
?n)))
%% “Restriction”
is a value of “domain” for “maxCardinality”.
(I.e., the first argument of maxCardinality is a restriction.)
(PropertyValue [maxCardinality axiom 1]
domain maxCardinality
Restriction)
%%
“NonNegativeInteger” is the value of “range” for “maxCardinality”. (I.e., the second argument of maxCardinality
is a non-negative integer.)
(PropertyValue [maxCardinality axiom 2]
range maxCardinality
NonNegativeInteger)
%% 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 “NoRepeatsLists” 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) [maxCardinality axiom 3]
(PropertyValue maxCardinality ?r ?n))
(forall (?i) (<=> (Type ?i ?r)
(forall (?vl)
(=> (and (NoRepeatsList ?vl)
(forall
(?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?i ?v))))
(=<
(length ?vl) ?n))))))[10]
%% Note that the
following can be inferred from the axioms regarding “maxCardinality” and “cardinality”:
(=> (and (PropertyValue maxCardinality
?r ?x) [maxCardinality theorem 1]
(PropertyValue cardinality ?r ?c))
(=< ?c ?x))
(=> (and (PropertyValue onProperty ?r
?p) [maxCardinality theorem 2]
(PropertyValue maxCardinality ?r 0))
(=> (Type ?x ?r) (not (PropertyValue ?p
?x ?v))))
%% “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 [cardinality axiom 2]
range cardinality
NonNegativeInteger)
%% 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
“NoRepeatsLists” 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) [cardinality axiom 3]
(PropertyValue cardinality ?r ?n))
(forall (?i) (<=> (Type ?i ?r)
(forall (?vl) (=> (and
(NoRepeatsList ?vl)
(forall
(?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?i ?v))))
(=
(length ?vl) ?n))))))
%% “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]
%% “Restriction”
is a value of “domain” for “minCardinalityQ”.
(I.e., the first argument of minCardinalityQ is a restriction.)
(PropertyValue [minCardinalityQ axiom 1]
domain minCardinalityQ
Restriction)
%%
“NonNegativeInteger” is the value of “range” for “minCardinalityQ”. (I.e., the second argument of minCardinalityQ
is a non-negative integer.)
(PropertyValue [minCardinalityQ axiom 2]
range minCardinalityQ NonNegativeInteger)
%% 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 “NoRepeatsList” 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) [minCardinalityQ axiom 3]
(PropertyValue minCardinalityQ ?r ?n)
(PropertyValue hasClassQ ?r ?c))
(forall (?i)
(<=> (Type ?i ?r)
(exists
(?vl)
(and (NoRepeatsList ?vl)
(forall (?v) (=>
(PropertyValue item ?vl ?v)
(and
(PropertyValue ?p ?i ?v)
(Type ?v ?c)))
(>= (length ?vl) ?n))))))
%% Note that the
following can be inferred from the axioms regarding “minCardinalityQ”,
“minCardinality”, “maxCardinalityQ”, and “cardinality”:
(=> (PropertyValue minCardinalityQ ?r
?n) [minCardinalityQ theorem 1]
(PropertyValue minCardinality ?r ?n))
(=> (and (PropertyValue [minCardinalityQ theorem
2]
minCardinalityQ ?r
?n)
(PropertyValue maxCardinalityQ ?r ?x))
(=< ?n ?x))
(<=> (PropertyValue cardinalityQ ?r
?n) [minCardinalityQ theorem 3]
(and (PropertyValue minCardinalityQ ?r ?n)
(PropertyValue maxCardinalityQ ?r
?n)))
%% “Restriction”
is a value of “domain” for “maxCardinalityQ”.
(I.e., the first argument of maxCardinalityQ is a restriction.)
(PropertyValue [maxCardinalityQ axiom 1]
domain maxCardinalityQ
Restriction)
%%
“NonNegativeInteger” is the value of “range” for “maxCardinalityQ”. (I.e., the second argument of maxCardinalityQ
is a non-negative integer.)
(PropertyValue [maxCardinalityQ axiom 2]
range maxCardinalityQ
NonNegativeInteger)
%% 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 “NoRepeatsLists” 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) [maxCardinalityQ axiom 3]
(PropertyValue maxCardinalityQ ?r ?n)
(PropertyValue hasClassQ ?r ?c))
(forall (?i) (<=> (Type ?i ?r)
(forall
(?vl)
(=> (and
(NoRepeatsList ?vl)
(forall
(?v)
(<=>
(PropertyValue item ?vl ?v)
(and (PropertyValue ?p ?i ?v)
(Type ?v ?c)))))
(=< (length ?vl)
?n))))))
%% Note that the
following can be inferred from the axioms regarding “maxCardinality” and
“maxCardinalityQ”:
(=> (PropertyValue maxCardinality ?r ?n) [maxCardinalityQ theorem 1]
(PropertyValue maxCardinalityQ ?r ?n))
%% “cardinalityQ”
is type “Property”.
(Type cardinalityQ Property) [cardinalityQ axiom 1]
%% “Restriction”
is a value of “domain” for “cardinalityQ”.
(I.e., the first argument of cardinalityQ is a restriction.)
(PropertyValue domain cardinalityQ
Restriction) [cardinalityQ axiom 2]
%%
“NonNegativeInteger” is the value of “range” for “cardinalityQ”. (I.e., the second argument of cardinalityQ is
a non-negative integer.)
(PropertyValue [cardinalityQ axiom 3]
range cardinalityQ
NonNegativeInteger)
%% 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 “NoRepeatsLists” 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) [cardinalityQ axiom 4]
(PropertyValue cardinalityQ ?r ?n)
(PropertyValue hasClassQ ?r ?c))
(forall (?i) (<=> (Type ?i ?r)
(forall
(?vl)
(=> (and
(NoRepeatsList ?vl)
(forall
(?v)
(<=>
(PropertyValue item ?vl ?v)
(and
(PropertyValue ?p ?i ?v)
(Type ?v ?c)))))
(= (length ?vl)
?n))))))
%% “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) [inverseOf axiom 1]
(and (Type ?p1 AbstractProperty)
(Type ?p2 AbstractProperty)
(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”:
(PropertyValue domain inverseOf
AbstractProperty) [inverseOf theorem 1]
(PropertyValue range inverseOf
AbstractProperty) [inverseOf theorem 2]
%% “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) [first axiom 2]
(and (Type ?l List) (PropertyValue _1 ?l
?x)))
%% Note that the
following can be inferred from the axioms regarding “first” and “item”:
(=> (PropertyValue first ?l ?x) [first theorem 2]
(PropertyValue item ?l ?x))
%% “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) [rest axiom 2]
(and (Type ?l List)
(Type ?r List)
(exists (?x) (= ?l (cons ?x ?r)))))[11]
%% Note that the
following can be inferred from the axioms regarding “oneOf”, “domain”, and
“range”:
(PropertyValue domain rest List) [rest theorem 1]
(PropertyValue range rest List) [rest theorem 2]
(=> (and (PropertyValue rest ?l ?r) [rest theorem 3]
(PropertyValue item ?r
?x))
(PropertyValue item ?l ?x))
%% “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) [item axiom 2]
(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”:
(PropertyValue domain item List) [item theorem 1]
%% “versionInfo”
is a property.
(Type versionInfo Property) [versionInfo axiom 1]
%% “imports” is a
property.
(Type imports Property) [imports axiom
1]
%% “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 axioms regarding “nil”, “first”, and “rest”:
(not (PropertyValue first nil ?x)) [nil theorem 1]
(not (PropertyValue rest nil ?x)) [nil theorem 2]
[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, 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.
[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] We do not use the properties “domain” and “range” in the RDF axioms since those properties are defined in RDF-S.
[8] We do not use the property “subClassOf” in the RDF axioms since “subClassOf” is a property defined in RDF-S.
[9] KIF note: “length” is a KIF function that denotes the number of items in the list denoted by the argument of “length”, and “>=” is the KIF relation for “greater than or equal”.
[10] KIF note: “=<” is the KIF relation for “less than or equal”.
[11] 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.