A Time Ontology

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₂ Î T_Li $s₁ Î T_L TRANS_L,Li(s₁,s₂)

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>

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.