A First-Order Logic Semantics for Semantic Web Markup Languages

Richard Fikes* Deborah McGuinness* Richard Waldinger#

*Knowledge
Systems Laboratory, Stanford University
#Artificial Intelligence Center, SRI International

Stanford, CA 94305 333 Ravenswood Avenue, Menlo Park, CA 94025

fikes@ksl.stanford.edu dlm@ksl.stanford.edu waldinger@ai.sri.com

Abstract

We present a case study in providing a declarative
semantics for three semantic markup languages being developed as ontology
representation languages for the Semantic Web by specifying for
each language an
equivalence-preserving translation into first-order logic (FOL). The translation includes for each language a
set of axioms that are included in the resulting FOL theories and that thereby constrain the
possible interpretations of those theories.
An important advantage of this form of semantics specification is that
the axioms can be tested for logical inconsistencies or redundancies, and for
whether they entail intended consequences.
We describe such tests that we have made on these axioms using existing
FOL reasoners. Also, we include a set
of theorems that express intended consequences of the axioms and that a FOL
reasoner can use to facilitate finding inconsistencies in and answering queries
from Semantic Web ontologies.

Introduction

In this paper, we present a
case study in providing a declarative semantics for three new knowledge
representation languages by specifying for each language an equivalence-preserving
translation of any given axiomatization
of a logical theory represented in the new language into an axiomatization of a
logically equivalent theory represented in an existing language for which a
declarative semantics is known. We
specify an equivalence-preserving translation into first-order logic for three
semantic markup languages being developed as ontology representation languages
for the Semantic Web: Resource Description Framework (RDF) [Lassila & Swick
1999, Lassila 1998], RDF Schema (RDF-S) [Brickley & Guha 2000], and
DAML+OIL [Hendler & McGuinness 2000; DAML 2001].

This method of providing a declarative semantics for a new representation language was described in [Van Baalen and Fikes 1994] in terms of translation into an interlingua. The method works for any target language of the translation for which there is a formal specification of a declarative semantics including logical entailment for which one can specify a translation and a set of top-level forms that satisfies the following definition:

**Definition
– interlingua-based semantics:** Let L
be a language, L_{i} be an interlingua language with a formally defined
declarative semantics, TRANS_{L,Li} be a binary relation between
top-level forms of L and top-level forms of L_{i}, and BT_{L}
be a set of top-level forms in L_{i}.
The pair <TRANS_{L,Li}, BT_{L}> is called an L_{i}-based
semantics for L when for every set T_{L} of top-level forms in L, there
is a set T_{Li} of top-level forms in L_{i} such that:

"s1 Î TL $s2 Î TLi TRANSL,Li(s1,s2)

"s_{2} Î T_{Li} $s_{1} Î T_{L} TRANS_{L,Li}(s_{1},s_{2})

And the theory represented
by T_{Li}ÈBT_{L} is equivalent to the theory represented by TL.

In
this definition, TRANS_{L,Li} specifies translations of top-level forms
in L to top-level forms in L_{i}.
Roughly speaking, BT_{L} is the set of axioms that are included
in the semantics of L expressed in L_{i}. When <TRANS_{L,Li}, BT_{L}> is being used
to define the semantics of L, then “the theory represented by T_{L}” is
equivalent to “the theory of T_{Li}ÈBT_{L}” *by definition*.

In our case study, L is either RDF, RDF-S,
or DAML+OIL, and L_{i} is first order logic (FOL). The top-level forms for FOL are
sentences. The primary claim of this
paper is that each of <TRANS_{RDF,FOL}, BT_{RDF}>, <TRANS_{RDF-S,FOL},
BT_{RDF-S}>, and <TRANS_{DAML+OIL,FOL}, BT_{DAML+OIL}>
can be included in the definition of the corresponding language accompanied by
the claim that it produces logically equivalent theories in FOL.

A model-theoretic semantics has been
proposed for RDF/S [Hayes 2001] and DAML+OIL [van Harmelen et al 2001]. Those semantics specifications are in the
traditional form in which an interpretation function is named for each
non-logical symbol in the language, and constraints are stated that must hold
for those interpretation functions.
This work complements those proposals and makes the following two
additional contributions.

A significant advantage of an
interlingua-based semantics for a representation language is that if such a
semantics is given in a machine-executable form (which it is here), the
semantics can be used to automatically translate the new language into the
interlingua. Hence, with a single
effort, one can give both a semantics for a new language and a procedure for
translating it into the interlingua.
Since in our case study the interlingua is first-order logic, the
translation produces a representation of the logical theory from which
inconsistencies can be found and queries can be answered automatically using
traditional automatic theorem provers and problem solvers. For example, the BT_{L} sentences
for DAML+OIL enable a first-order-logic theorem prover to infer from the two
statements “Class Male and class Female are disjoint.” and “John is type Male.”
that the statement “John is type Female.” is false.

Another significant advantage of an
interlingua-based semantics is that the constraints imposed by the source
representation language on the interpretation of logical theories represented
in that language are expressed as axioms in the interlingua. If automated reasoning tools are available
for the interlingua, which they are for our case study in which the interlingua
is first-order logic, one can then subject the BT_{L} axioms to
critique using those tools to discover inconsistencies, unintended
consequences, missing or overly weak axioms, redundant axioms, or needlessly
complex axioms. Many of these problems
can escape detection even after prolonged intense public scrutiny and social
process.

The Translation To FOL

We proceed by specifying the
translation TRANS_{L,FOL} and the FOL sentences BT_{L} for each
of the three new representation languages.
TRANS_{L,FOL} turns out to be trivial for all three languages so
that the primary task is creating the semantics BT_{L} for the
languages.

RDF is defined in terms of an abstract data
model in which the top-level forms are triples, called *statements*, of
the form <property, subject, object> (Section 2.1 [Lassila & Swick
1999]). RDF, RDF-S, and DAML+OIL are
subsets of each other in the sense that RDF-S is RDF plus a set of non-logical
constants (i.e., an ontology) and DAML+OIL is RDF-S plus an additional set of
non-logical constants. Therefore, the
top-level forms of all three languages can be considered to be RDF statements. The languages differ only in that RDF-S and
DAML+OIL provide additional predefined terminology (properties, classes, and
objects) to RDF. Thus, it is sufficient
for all three languages to define a translation from RDF triples to FOL
sentences.

The concrete syntax for these languages will
typically be something other than <property, subject, object> triples.[1] Thus, in general, the first step of the
translation into FOL will be a translation from a concrete syntax into RDF
statements. The only requirement we
impose on that first translation step is that each element of the RDF
statements it produces be labeled such that each label is a URI or a literal as
given in the concrete syntax or a skolem constant generated by the translator
for an element that is not labeled in the concrete syntax. Each label generated for an unlabeled
statement element must be distinct from all other labels.[2]

The translation TRANS_{L,FOL} for L
being RDF, RDF-S, or DAML+OIL from the abstract data model of L is defined
simply as follows

TRANS_{L,FOL}(<property, subject,
object>) :=

(PropertyValue property subject object)

This translation is designed to place
minimal constraints on the interpretation of the non-logical symbols in the
translated logical theory and to enable the required BT_{L} axioms to
be expressible in first-order logic. In
particular, it does not translate properties into binary relations. The translation therefore enables axioms
that apply to all properties (i.e., that use a universally quantified variable
for the property) to be stated without quantifying over the relation in a
relational sentence and hence to be expressible in first-order logic. If one is willing to consider properties to
be binary relations, the axioms can be stated in first-order logic by
translating each RDF triple “<property, subject, object>” into “(holds
property subject object)” rather than using the relation PropertyValue,
assuming there is an appropriate formalization and semantics for “holds” (See
Section 2.1 [Hayes 2001]).

In order to consider a given property p to be a binary relation without using “holds”, one can simply add to BTL the following axiom:

(<=> (PropertyValue p ?x
?y) (p ?x ?y))[3]

Also, in order to consider a given class C to be a unary relation without using “holds”, one can add to BTL the following axiom:

(<=> (PropertyValue type
?x C) (C ?x))

If properties are being translated into binary relations and classes into unary relations, one could use these two axioms to add to BTL an axiom for each property and class that is included in the definition of L (e.g., “Resource”, “type”, etc. for RDF; “ConstraintResource”, “subClassOf”, etc. for RDF-S; and “Restriction”, “onClass”, etc. for DAML+OIL) and thereby make the axioms in BTL more concise and readable.

The FOL Axioms

The axioms BT_{L} added to the
translation of the RDF statements in a knowledge base[4]
are designed to reflect the layering of RDF, RDF-S, and DAML+OIL in the sense
that the axioms BT_{RDF} do not use the properties or classes of RDF-S
or DAML+OIL, the axioms BT_{RDF-S} use the properties and classes of
RDF but do not use the properties or classes of DAML+OIL, and the axioms BT_{DAML+OIL}
use the properties and classes of both RDF and RDF-S. Also, since the three languages are subsets of each other, BT_{RDF}
Ì BT_{RDF-S} Ì BT_{DAML+OIL}. The complete set of axioms is included in [Fikes & McGuinness
2001].

The BT_{L} axioms for each of the
three languages are designed to minimize the constraints on the interpretation
of the non-logical symbols in the resulting logical theory and the requirements
on a reasoner making deductions from the T_{FOL}ÈBT_{L} knowledge base. In particular, the axioms do not require set
theory-based reasoning, they do not require classes be considered to be sets or
to be unary relations, and they do not 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
knowledge bases being translated.

Because of the pervasiveness of axioms in
the BT_{L} of all three languages about values of the RDF property
“type”, we have for convenience defined a binary relation “Type” and added the
following axiom to BT_{RDF}:

(<=> (Type ?x ?c)
(PropertyValue type ?x ?c))

Note that this addition provides
us with a shorthand for expressing values of property “type” without requiring
that “type” be a relation. We use that
shorthand throughout BT_{RDF}, BT_{RDF-S}, and BT_{DAML+OIL}.

The Axioms for RDF

The BT_{RDF} axioms
include statements that the first argument of relation PropertyValue must be a
property; that Property and rdfs:Class have no instances in common (i.e., they
are disjoint classes); that an RDF statement has exactly one property, one
object, and one subject; and that a container is a Seq, a Bag, or an Alt.

The Axioms for RDF-S

The BT_{RDF-S} axioms
include statements that ConstraintResource is a subclass of Resource, that a
property is a ConstraintProperty if and only if it is also a Constraint
Resource, that an instance of a subclass is also an instance of the superclass,
that a value of a subProperty is also a value of the superProperty; that
ConstraintProperty is a subclass of Property; that a value of a property must
be an instance of the range of that property; and that an object that has a
value for a property must be an instance of the domain of that property.

The Axioms for DAML+OIL

The BT_{DAML+OIL} axioms are significantly
more extensive than either BT_{RDF} or BT_{RDF-S}. They include statements that extend the
subclass and subproperty taxonomies; that specify domain and range constraints
for all the DAML+OIL classes and properties; that define the class of all
objects (Thing), the empty class (Nothing), the class of properties that are
transitive, the class of properties that can have at most one value for a given
object, the class of properties that can have a given value for at most one
object, the class of properties that assert classes are disjoint, the class of
properties that assert that properties are inverses of each other, and a class
of properties that assert classes are complements of each other; that define
the class of properties that assert the equivalence of objects, classes, and
properties; that define properties that assert that a class is a union,
intersection, or disjoint intersection of a list of classes; that define the
various kinds of restrictions; and that define lists and their associated
properties

Axiomatizing Cardinality Restrictions

One of the challenges in
writing the BT_{DAML+OIL} axioms was axiomatizing the various cardinality
restrictions in DAML+OIL (minCardinality, maxCardinalityQ, etc.) without adding
a set theory. We met that challenge by
writing a simple axiomatization of tuples and their length and then defining a
type of tuple that has no repeating elements, as shown in Figure 1. In those axioms, we define the empty tuple EmptyTuple, the binary relation Item,
the unary functions First, Rest, and Length, the binary function 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 maps a nonempty tuple
to the tuple consisting of its 2^{nd} 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.

Given those relations, we then wrote axioms for each of the cardinality restrictions, such as the one for cardinality shown in Figure 2, which expressed a constraint on the length of a NoRepeatsTuple that contains all the values of a given property at any one object.

** **

%% Item is a binary relation that relates a tuple to
its elements.

(=> (Type ?t Tuple)

(<=> (Item ?t ?x)

(and (not (= ?t EmptyTuple))

(or (= (First ?t) ?x)

(item (Rest ?t) ?x)))))

%% The length of a tuple is the number of elements
in the tuple.

(Length EmptyTuple 0)

(=> (Type ?t Tuple)

(= (Length (Cons ?x ?t))

(+ 1 (Length ?t))))

%% A NoRepeatsTuple is a tuple for which no item
occurs more than once.

(<=> (NoRepeatsTuple
?t)

(and (Type ?t Tuple)

(or (= ?t EmptyTuple)

(= (Rest ?t) EmptyTuple)

(and (not (Item (Rest ?t)(First ?t))

(NoRepeatsTuple (Rest ?t)))))

Figure 1: Tuple Axiomatization

(=>(and

(PropertyValue onProperty ?r ?p)

(PropertyValue cardinality ?r ?n))

(forall (?i)

(<=> (Type ?i ?r)

(exists (?vl)

(and (NoRepeatsTuple ?vl)

(forall (?v)

(<=> (Item ?vl ?v)

(PropertyValue ?p ?i ?v)))

(= (Length ?v1)?n)))))** **

Figure 2: Cardinality Axiomatization

Example Translation and Inference

Consider the following
DAML-OIL descriptions in XML syntax of class **“**Person” and of a person
“Joe”:

<daml:Class rdf:ID = "Person">

<rdfs:subClassOf rdf:resource = "#Animal" />

<rdfs:subClassOf>

<daml:Restriction>

<daml:onProperty rdf:resource = "#hasParent" />

<daml:toClass rdf:resource = "#Person" />

</daml:Restriction>

</rdfs:subClassOf>

</daml:Class>

<Person rdf:ID = "Joe">

<hasParent rdf:resource = "#John” />

</Person>

Informally,
the descriptions say that a person is an animal all of whose parents are
persons, and Joe is a person one of whose parents is John. Formally, they say that Person is a class that is a subclass of class Animal and a subclass of an unlabeled Restriction that has hasParent as a
value of property onProperty and Person as a value of
property toClass, and that Joe is a Person that has John as a
value of property hasParent.

Those descriptions produce a knowledge base of the following RDF statements:

(rdf:type daml:Class Person)

(rdfs:subClassOf Person Animal)

(rdfs:subClassOf Person GenR)[5]

(rdf:type daml:Restriction GenR)

(daml:onProperty GenR hasParent)

(daml:toClass GenR Person)

(rdf:type Joe Person)

(hasParent Joe John)

Those statements are
translated by TRANS_{DAML+OIL,FOL} into the following sentences:

(Type daml:Class Person)

(PropertyValue rdfs:subClassOf Person Animal)

(Type daml:Restriction GenR)

(PropertyValue rdfs:subClassOf Person GenR)

(PropertyValue daml:onProperty GenR parent)

(PropertyValue daml:toClass GenR Person)

(Type Joe Person)

(PropertyValue Parent Joe John)

An FOL reasoner should be
able to infer from these sentences and BT_{DAML+OIL} that “John” is
type “Person”. That inference can be
made by first inferring that “John” is type “GenR” by using the following
subClassOf axiom:

(<=> (PropertyValue

subClassOf ?csub ?csuper)

(and (Type ?csub rdfs:Class)

(Type ?csuper rdfs:Class)

(forall (?x)

(=> (Type ?x ?csub)

(Type ?x ?csuper)))))

That axiom says that csub is
a subclass of csuper if and only if csub is a class, csuper is a class, and for
all x if x type csub then x is type csuper.
If the reasoner substitutes “Person” for ?csub and “GenR” for ?csuper,
the axiom can be used to infer the following:

(=> (PropertyValue

subClassOf Person GenR)

(=> (Type Joe Person)

(Type Joe GenR)))

Since “(PropertyValue subClassOf
Person GenR)” and “(Type Joe Person)” are given, the reasoner can then infer “(Type Joe GenR)”. The
reasoner can then use toClass axiom 3 to infer that “John” is type “Person” as
follows. The axiom is:

(=> (and (PropertyValue

onProperty ?r ?p)

(PropertyValue toClass ?r ?c))

(forall (?i)

(<=> (Type ?i ?r)

(forall (?j)

(=> (PropertyValue

?p ?i ?j)

(Type ?j ?c))))))

The
axiom says that if R is a toClass restriction on class C for property P, then
for all I, I is type R if and only if all values J of P are type C.

If the
reasoner substitutes “GenR” for ?r, “hasParent” for ?p, “Person” for ?c, and
“Joe” for ?I, the axiom can used to infer:

(forall (?j)

(=> (PropertyValue hasParent Joe ?v)

(Type ?v Person)))

If the reasoner substitutes
“John” for ?j in that intermediate result, it can infer:

(Type John Person)

This is what we set out to prove. Our proof may be generated without using standard tableaux methods used in modern description logics[Horrocks & Sattler 2001]. That can be viewed as a benefit to those attempting to present a (possibly pruned) trace through the system deductions in order to provide an explanation of the reasoning. Explanation in description logics was first provided for systems that did not use tableaux reasoning [McGuinness 1996] and was later adapted for a tableaux-based system [Borgida et al 1999]. It is argued that proofs not relying on the negations used in the tableaux process may be more understandable to users.

Theorems To Facilitate Automatic Reasoning

A primary motivation for
developing a translation of these languages into FOL was to facilitate
automatic query-answering (i.e., deductive retrieval of objects that match a
given set of constraints) from a DAML+OIL knowledge base. Many of the axioms as written would be very
difficult for a reasoner to use directly.
We have therefore produced a set of theorems THL that are inferable from
the BTL axioms for each of the three languages RDF, RDF-S, and DAML+OIL. The theorems are included in the axiom
document:
http://www.ksl.stanford.edu/people/dlm/daml-semantics/abstract-axiomatic-semantics.html.

The theorems have the
following properties:

• They are all either Horn clauses with RDF statements as atoms, or implications in which a conjunction of atoms (i.e., RDF statements) implies FALSE.

• They are intended to state all of the RDF statements that can be inferred about the constants that are explicitly mentioned in the knowledge base or are defined in the language in which the knowledge base is represented (i.e., either RDF, RDF-S, or DAML+OIL). So, for example, the theorems express a consequence that an object is not an instance of a class only if the complement of the class is already a named class in the knowledge base so that the consequence can be expressed as the object being an instance of the complement.

The theorems can be
considered to be a set of intended consequences from the axioms expressed in
forms that are directly useable by traditional FOL reasoners. Any additional intended consequence that a
FOL reasoner is having difficulty making can be expressed in the form of an
implication, and a theorem prover can be used to attempt to prove the
implication from the axioms. If the
proof succeeds, then the implication is a theorem and can be used directly in
future reasoning to infer the intended consequence.

The most important of the theorems in terms of facilitating reasoning are the theorems involving the various cardinality restrictions. The axioms that define the semantics of the cardinality restrictions are expressed in terms of the lengths of “no repeats tuples” whose elements are values of a given property for a given object. Those axioms do not easily lend themselves to making the standard inferences about inconsistent cardinality restrictions (e.g., when a max cardinality restriction is less than a corresponding min cardinality restriction), about equality of property values (e.g., when there are two values of a property for an object that has a max cardinality restriction of 1), etc. The theorems support each of those standard inferences by providing an implication whose use will enable a reasoner to directly make the desired conclusion.

Validation of the Axioms

As discussed above in the
introduction, a significant advantage of an interlingua-based semantics for a
language L is that the BT_{L} axioms can be subjected to critique using
automated reasoning tools to discover inconsistencies, unintended consequences,
missing or overly weak axioms, redundant axioms, or needlessly complex
axioms. In our case study, we are
critiquing each of the three sets of BT_{L} axioms using a combination
of the Specware [Specware] software development environment of the Kestrel
Institute, the theorem prover SNARK [Stickel], developed at SRI International,
and (to a lesser extent) the theorem prover Gandalf [Tammet], from Chalmers.

Specware has a graphical user interface that
displays the axioms in a theory, a set of conjectures, and a set of proved
theorems, and enables a user to select a conjecture to be proved and to alter
the settings on the chosen theorem prover.
Specware can translate the theory, including the conjecture, into the
language of the chosen theorem prover, which then attempts to prove the conjecture,
and reports the results back to Specware, which updates the theory
accordingly. When searching for
inconsistencies, we attempt to prove the conjecture false.

Using such reasoning tools, one can subject a FOL knowledge base to a number of tests. While no test can guarantee the correctness of axioms, we can uncover problems in them and build increased confidence that they reflect our intentions. Here are some of the tests that can be performed:

**Logical Inconsistencies** – One can ask the reasoner to deduce false from a knowledge base. Examining the proof will pinpoint the axioms responsible for the
inconsistency. Under the intended model
for DAML, at least one of those axioms must be false.

**Redundancies** – One can determine whether a knowledge base contains
redundancies by sequentially removing each axiom Ai from the knowledge base and
asking the reasoner to deduce Ai from the knowledge base resulting from the
removal of Ai. Any such Ai that is
deduced is a redundant axiom and can be either omitted or designated as a
theorem. Also, in searching for
inconsistencies, the reasoner will report if any axiom is subsumed by the
others; these may safely be removed.

**Intended Consequences** – One can conjecture consequences that one intends a
knowledge base to entail and ask the reasoner to deduce each such conjecture
and its negation. The theorems included
with the axioms discussed in the previous section are an example of such
intended consequences. The reasoner’s
inability to prove an intended consequence is a cause for concern and can be
investigated by asking the reasoner to prove a sequence of lemmas that one
expects would be used in a proof of the intended consequence to determine where
the proof attempt failed. Similarly, if
the negation of an intended consequence is deduced, one can conclude that
changes need to be made in the axioms used in that deduction.

All of these tests have been applied to earlier versions of the axioms for RDF, RDF-S, and DAML+OIL using Specware and SNARK, and instances of all the above problems have been uncovered and corrected. We are in the process of repeating the tests on the current version of the axioms and theorems.

There are several limitations, theoretical and practical, to this kind of validation process. Consistency of a knowledge base cannot be guaranteed. Since the problem of determining the consistency of a FOL knowledge base is not decidable, failure to find an inconsistency in any finite amount of time cannot be taken as a proof of consistency. One could deal with this problem in a relative way by mapping the theory into another, accepted theory, whose consistency is assumed.

Similarly, failure to produce a proof of a
conjecture cannot be taken as logical evidence that the conjecture is
false. (There are cases in which a
complete theorem prover will halt after exhausting all possibilities of finding
a proof, implying that the conjecture is not a theorem. This is exceptional and
doesn't happen in the BT_{DAML+OIL} knowledge base.)

Finally, correctness of the theorem prover
itself is not guaranteed. One can
reduce that doubt by reproducing the proof with many theorem provers (e.g.
JTP[JTP], SNARK[Stickel], Gandalf[Tammet]).
However, one cannot eliminate it.
In practice, bugs in theorem provers that lead to proofs of invalid
results (i.e., unsoundness) are quite rare.

Example Validation Test

In this section, we present a
test that has been run on the current version of BT_{DAML+OIL}. The test is taken from the DAML Structured
Walkthru [van Harmelen et al 2001b] and is to determine whether an intended
consequence of a cardinality restriction is deducible from BT_{DAML+OIL}. Specifically, let OneFatherClass be the restriction whose onProperty is the property hasFather that holds between an object and its father, and
whose cardinality parameter is 1. Then it is an intended consequence of the
axioms that OneFatherClass is the class of all elements that have exactly one
father. We then assert that

Person is a subclass of OneFatherClass. Then
we should be able to conclude that every Person has
precisely one father. In particular, we
expect to be able to infer that

- Every Person
has a father.
- No Person has two distinct fathers.

Furthermore, we expect that

· If an element has precisely one father, that element is a member of OneFatherClass.

While these conjectures can be proved quickly by SNARK from the latest cardinality axioms, earlier versions of the axioms had an undetected flaw such that SNARK could not prove the second and third of these conjectures. This failure led to the discovery and correction of the flaw of the axiom, which was represented in FOL (and was not representable in a more limited language such as DAML+OIL).

Many other flaws were detected in the
original axiom set and even in the axioms for KIF[KIF], which have been
published and widely used since 1998.
The original axiom for First, for example, had a
quantifier error, so that it actually implied that any two elements were
equal. This made the axiom inconsistent
with any axiom that implied that two elements were distinct (e.g., that (not (0 = 1)).) Another
quantifier error, in the definition of FunctionalProperty, also caused the
theory to be inconsistent. These errors
were undetected until SNARK deduced false from the
Specware version of the axiom set.
Examining the refutation allowed us to pinpoint the source of the error
and correct it.

A number of axioms were found to be redundant when SNARK announced, in the course of searching for inconsistencies, that they were subsumed by other axioms. Other axioms, not detected by the subsumption check, were eliminated when it was conjectured and proved that they were implied by the others. Some axioms were found to be simplified by the theorem prover. These results are described in more detail in [Consistency Checking and Automated Theorem Proving by the UBOT Project, http://vis.home.mindspring.com/daml/HotVIS.htm].

While we have not yet run a consistency
check on the entire current set of axioms, the axioms defining the various
kinds of cardinality restrictions have resisted earnest attempts to find
contradictions.

Summary

We have presented a case
study in providing a declarative semantics for three semantic markup languages
being developed as ontology representation languages for the Semantic Web by
specifying for each language an equivalence-preserving translation into
first-order logic. The translation
includes for each language a set of axioms that are included in the resulting
FOL theories and that thereby constrain the possible interpretations of those
theories. An important advantage of
this form of semantics specification is that the axioms can be tested for
logical inconsistencies and redundancies, and for whether they entail intended
consequences. We described such tests
that we have made on these axioms using existing FOL reasoners. Also, we have included a set of theorems
that express intended consequences of the axioms and that a FOL reasoner can
use to facilitate finding inconsistencies in and answering queries from
Semantic Web ontologies.

**Acknowledgement:** The authors are indebted to DARPA for their support
under contracts F30602-00-2-0579,
F30602-00-C-0168 ( K533), and F30602-00-C-0188. The **authors also gratefully acknowledge
the useful comments** of Pat Hayes,
Peter Patel-Schneider, Ian Horrocks,
and members of the UBOT and SRI DAML projects, in conversations concerning the
work. This work extends two of the
authors’ work on our original axiomatic semantics proposal for DAML+OIL [Fikes
& McGuinness 2001] and earlier work on DAML-ONT [McGuinness et al 2002].

References

[van Baalen & Fikes] Jeff Van Baalen
and Richard Fikes; “The Role of Reversible Grammars in Translating Between
Representation Languages”; Proceedings of the 4th International Conference on
Principles of Knowledge Representation and Reasoning; Bonn, Germany; May 1994;
pages 562-571. (http://www.ksl.stanford.edu/KSL_Abstracts/KSL-93-67.html).

[Borgida et al 1999] Alex Borgida, Enrico Franconi, Ian Horrocks, Deborah L. McGuinness, and Peter Patel-Schneider. “Explaining ALC Subsumption”. Proceedings of the International Description Logics Workshop, pp 33-36, Linköping, Sweden, July 1999.

[Bray et al 2000] Tim Bray, Jean Paoli, C. Sperberg-McQueen, and Eve
Maler. Extensible Markup Language
(XML) Second Edition W3C Recommendation October 6, 2000. Available online as http://www.w3.org/TR/REC-xml .

[Brickley & Guha 2000] Dan Brickley
& R.V.Guha, "Resource Description Framework (RDF) Schema Specification
1.0", W3C Candidate Recommendation 27 March 2000, World Wide Web
Consortium, Cambridge (MA); available on-line as http://www.w3.org/TR/rdf-schema/
.

[DAML] Ian Horrocks, Frank van Harmelen,
Peter Patel-Schneider, Tim Berners-Lee, Dan Brickley, Dan Connolly, Mike Dean,
Stefan Decker, Dieter Fensel, Pat Hayes, Jeff Heflin, Jim Hendler, Ora Lassila,
Deborah McGuinness, and Lynn Andrea Stein.
DAML+OIL, March 2001. Available
online at: http://www.daml.org/2001/03/daml+oil-index.

[Fikes & McGuinness 2001] Richard
Fikes and Deborah L. McGuinness. “An
Axiomatic Semantics for RDF, RDF Schema, and DAML+OIL''. Stanford University Knowledge Systems
Laboratory Technical Report KSL-01-01, 2001.
Available at: http://www.ksl.stanford.edu/people/dlm/daml-semantics/abstract-axiomatic-semantics.html
and from the DAML website: http://www.daml.org/2001/03/daml+oil-index.

[van Harmelen et al 2001] Frank van Harmelen, Peter
Patel-Schneider, and Ian Horrocks, editors.
“A Model Theoretic Semantics for DAML+OIL”, March 2001. Available online at: http://www.daml.org/2001/03/model-theoretic-semantics.html
.

[van Harmelen et al 2001b] Frank van
Harmelen, Peter Patel-Schneider, Ian Horrocks, Dan Connolly, Lynn Stein, and
Deborah McGuinness, editors.
Annotated DAML+OIL Ontology
Markup. March 2001. Available at: http://www.daml.org/2001/03/daml+oil-walkthru.html
.

[Hayes 2001] Patrick Hayes, editor. “RDF Model Theory “, W3C Working Draft 25
September 2001. Available online at: http://www.w3.org/TR/rdf-mt/ .

[Hendler & McGuinness 2000] James
Hendler and Deborah McGuinness. ``The DARPA Agent Markup Language''. In IEEE
Intelligent Systems Trends and Controversies, November/December 2000. Available from http://www.ksl.stanford.edu/people/dlm/papers/ieee-daml01-abstract.html
.

[Horrocks and Sattler 2001] Ian Horrocks
and Ule Sattler. Ontology reasoning in
the SHOQ(D) description logic. In B. Nebel, editor, Proc. of the 17th Int.
Joint Conf. on Artificial Intelligence (IJCAI-01), pages 199-204. Morgan
Kaufmann, 2001.

[JTP] http://www.ksl.stanford.edu/software/JTP/.

[KIF] http://logic.stanford.edu/kif/kif.html
.

[Lassila 1998] Ora Lassila, "Web
Metadata: A Matter of Semantics", IEEE Internet Computing 2(4): 30-37
(1998).

[Lassila & Swick 1999] Ora Lassila
& Ralph Swick, "Resource Description Framework (RDF) Model and Syntax
Specification", W3C Recommendation 22 February 1999, World Wide Web
Consortium, Cambridge (MA); available on-line as http://www.w3.org/TR/REC-rdf-syntax/.

[McGuinness 1996] Deborah L.
McGuinness. “Explaining Reasoning in
Description Logics”. Ph.D. Thesis,
Rutgers University, 1996. Technical Report LCSR-TR-277.

[McGuinness et al 2002] Deborah L. McGuinness, Richard Fikes, Lynn Andrea Stein, and James Hendler. ``DAML-ONT:
An Ontology Language for the Semantic Web ''. To appear in Dieter Fensel, Jim
Hendler, Henry Lieberman, and Wolfgang Wahlster, editors. The Semantic Web:
Why, What, and How, MIT Press, 2001.
Preprints available at: http://www.ksl.stanford.edu/people/dlm/papers/daml-ont-abstract.html
.

[Stickel] Mark E. Stickel, Richard J.
Waldinger, Vinay K. Chaudhri. “A Guide
to SNARK”. http://www.ai.sri.com/snark/tutorial/tutorial.html

[Specware] http://www.specware.org/

[Tammet] Tanel Tammet. “Gandalf family of automated theorem
provers”. http://www.cs.chalmers.se/~tammet/gandalf

[1] For example, the RDF
specification [Lassila & Swick 1999] describes an Extensible Markup
Language [Bray et al 2000] encoding as the concrete syntax for RDF.

[2] See [Hayes 2001] Section 3.1
for a discussion of substituting skolem functions for unlabeled subjects and
objects in RDF.

[3] We use the KIF syntax for
FOL sentences in this paper. In that
syntax, the symbol “<=>” means “if and only if”.

[4] In this paper, we will refer
to an axiomatization of a logical theory as a *knowledge base*.

[5] “GenR” is the generated label for the unlabeled
restriction.