Knowledge Systems Laboratory
Abstract: "An Axiomatic Semantics for RDF, RDF Schema, and DAML+OIL"
Richard Fikes and
Deborah L. McGuinness.
``An Axiomatic Semantics for RDF, RDF Schema, and DAML+OIL''
KSL Technical Report KSL-01-01, 2001. Updated August, 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
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.
are both vocabularies of non-logical symbols added to RDF, the translation of
RDF statements is sufficient for translating RDF Schema and DAML+OIL as well.
The axioms are written in ANSI Knowledge Interchange Format (
KIF)), which is a proposed ANSI standard.
The full paper is available in
In order to support additional operational use of the document,
we include two additional files:
one containing all of the
in the document.
This replaces the previous axiomatic semantics for DAML+OIL and the previous axiomatic semantics for DAML-ONT which are available
The main differences in this version over the previous version are listed below:
- The theorems in the document have been significantly revised to
facilitate the use of the axioms for automatic reasoning. In the new
version, the theorems are all either (1) KIF representations of RDF
statements that one can assume to be included in any knowledge base, (2)
KIF versions of Horn clauses with RDF statements or evaluable
constraints as atoms, or (3) implications in which a conjunction of
atoms (i.e., KIF representations of RDF statements or evaluable
constraints) implies FALSE. For example, these theorems could be used
by a forward chaining mechanism to infer additional assertions or
logical inconsistencies while a DAML+OIL knowledge base is being loaded.
A file containing only the axioms and a file containing only the
theorems has been linked to the primary document to facilitate loading
the axioms and theorems into a reasoner.
The numbering scheme for the axioms and theorems was changed so that
the number associated with an axiom or theorem does not change every
time an axiom or theorem is added to or deleted from the document.
Bugs and redundancies in the axioms and theorems that were reported to
us were fixed.
Publications of Richard Fikes,
Selected Publications of Deborah L. McGuinness.