The three SWeb languages so far given W3C 'recommendation' status (RDF [RDF], RDFS [RDFS] and OWL[Webont]) can all be translated straightforwardly into Common Logic [CL]. This document gives full translations, showing how to express all of the content of these languages directly in CL.

Very little of this is new or original. The translations follow a number of standard conventions: classes map into unary relations, properties into binary relations, and expression forms in OWL and RDFS map into particular patterns of quantification applied to boolean combinations of atoms built from these relations. These more elaborate languages (i.e RDF semantic extensions, c.f. [RDF-Semantics]) also require adding axioms which describe their semantic assumptions explicitly; this is along the lines used by Fikes and McGuinness [Fikes&McGuinness] in their 'axiomatic semantics' for DAML (the precursor to OWL) and later suggested in a W3C note [Lbase]. Datatyped literals are handled by using functions representing the datatypes, in a uniform way.

Throughout this document, examples of RDF, RDFS and OWL text are rendered in italics, while CL text is rendered as code. Three-letter strings such as sss, ppp are used to indicate generic components of expressions, and when giving translations (usually in the form of tables) a change of rendering indicates the application of the translation in question, so that if ppp indicates some expression in RDF or OWL, then ppp indicates the result of translating that expression into CL syntax using the conventions in the table. The Common Logic CLIF syntax [CL] and the N-triples notation for RDF [RDFTestCases] are used throughout.

TWO LOGICAL STYLES: TRANSLATION vs. EMBEDDING

RDF, RDFS and OWL use a large vocabulary of special names to express meanings which would often be expressed directly in logic by writing a sentence. For example, the OWL/RDF triple

ex:foo rdf:type owl:TransitiveProperty .

carries the meaning that ex:foo is a transitive binary relation, which would naturally be expressed in logic by writing a sentence

(forall (x y z)(implies
    (and (ex:foo x y)(ex:foo y z))
      (ex:foo x z)
))

without using the term "owl:TransitiveProperty". Translating such languages into logic can be done in two rather different ways, therefore. One style (as used for example in [Lbase]) replaces the specialized RDFS and OWL vocabulary by logical sentences which capture their intended meaning, illustrated by the above example; we will refer to this as translation. The other style (as used for example in [Fikes&McGuinness]) reproduces the RDF/RDFS/OWL triples in the logic more or less directly, preserving the special names, and then relates them to their logical meanings by axioms. We will refer to this as embedding the RDF/RDFS/OWL in logic. For example, an embedding of the above triple would be a single atomic sentence

(rdf_triple ex:foo rdf:type owl:TransitiveProperty)

but the embedding would utilize additional axioms such as

(forall (x y z)(iff (rdf_triple y x z)(x y z)))

(forall (x y) (iff (rdf:type x y)(y x)))

(forall (p) (iff
    (owl:TransitiveProperty p)
    (forall (x y z)(implies (and (p x y)(p y z))(p x z) ))
))

to connect the embedded triple-atom to the sentence which defines its meaning.

The choice of one style rather than the other has produced some controversy, as they result in incompatible translations in a conventional first-order logical syntax, and moreover the translation may produce ill-formed logical expressions in some cases; for example, the rdf-valid RDF triple

rdf:type rdf:type rdf:Property .

maps into the logical sentence

(rdf:type rdf:type rdf:Property)

which is syntactically illegal in most first-order presentations, though not in CL; for this reason, the embedding style is often used to process RDF/RDFS/OWL by logical inference engines, even though it does not exhibit the natural logical structure. CL however is more flexible in its syntax than most conventional logics, and has devices which supply a form of tail-recursion; so in many cases - all of RDF/RDFS and much of OWL - it is possible to state in CL the equivalence of the two styles, and use them interchangeably. We will take advantage of this when giving the embeddings, to make the axioms more readable; and when giving the translations, to make the logical meaning more vivid.

Nevertheless, the two styles do have clear pros and cons. Translation is shorter and more transparent to define, and likely to be far more efficient in practice. (In effect, embedding amounts to using CL reasoning to do the translation, a job that is likely best left to a more efficient implementation technique.) On the other hand, the fact that an embedding retains the specialized RDFS/OWL vocabulary means that it can succinctly state many RDFS and OWL truths which would be inexpressible wihout that vocabulary. For a simple example, the fact that

ex:p rdf:type owl:FunctionalProperty .
ex:p owl:inverseOf ex:q .

together OWL-entail

ex:q rdf:type owl:InverseFunctionalProperty .

can be checked in a translation by determining that their translations logically entail one another; but it cannot be directly expressed in the translated form; whereas, the embedding provides the vocabulary needed to express it directly as a lemma (which could be derived from the embedding):

(forall (p q) (implies
    (and (owl:FunctionalProperty p)(owl:inverseOf p q))
    (owl:InverseFunctionalProperty q)
))

In this document we provide both translations in the form of translation tables, and axioms suitable for use with an embedding strategy.

RDF

RDF Triples

A simple RDF triple s p o . is embedded into CL as (rdf_triple s p o) and translates into the atomic sentence (p s o).

In CL these are completely compatible, and the relationship between them can be expressed axiomatically in the language, by a sentence which we will adopt here as axiomatic:

(forall (x y z)(iff (rdf_triple y x z)(x y z)))

The presence of this axiom ensures that translations formed using the two styles are equivalent, so the styles may be used interchangeably.

This axiom is based on the premis that all binary relations have the status of RDF properties; and since in CL any term may be used as a relation, this means that everything in the universe is an RDF property. We will call this (and its variations, later) the promiscuity assumption: it amounts to using the syntactic freedom of CL to assign every status to every symbol, in effect denying any attempt to categorize the universe into exclusive classes or categories. This is quite appropriate to RDF, which has a similarly laissez-faire attitude to syntactic typing; however, OWL-DL relies on such categorizations, so we will be obliged to modify the promiscuity assumption when we consider the OWL class of languages. We will therefore modify the axiom by qualifying it and then rendering the qualification (temporarily) vacuous:

One could rationally deny promiscuity, of course, and insist that there are binary relations which are not RDF properties, so that it would then be quite consistent to assert for example

(and (Rel this that) (not (rdf:Property Rel)))

where the relation Rel is considered to be "external" to RDF and so cannot be represented in an RDF graph. To use this cautious option, we would remove the promiscuity axiom and replace it with a case-by-case addition of the necessary assumptions as part of the translation:

We will refer to this as the 'cautious approach', and adopt it when translating official OWL, since OWL requires some distinctions to be made between the OWL and RDFS universes. Until further notice, however, we will assume promiscuity in order to keep the translations simpler. It is straightforward (though tiresome) to introduce the explicit qualifications where needed.

Note that the added conditions - in this case, the fact that ppp is indeed an RDF property - are all valid in the source language, and so do not represent any 'extra' assumptions made in the translation.

RDF Literals

Literals in RDF are of two types: plain literals and typed literals. Plain literals translate into CL quoted strings, possibly paired with a language tag, and in both RDF and CL they are understood to denote themselves. We use the function stringInLang to indicate the pair consisting of a plain literal and a language tag. (Note. At the time of writing, it is unclear whether or not the XML designers intend that a string with a language tag is considered to be identical to the string or not. Either view could be expressed as CL axioms, but we here deliberately avoid making this committment either way.) Typed literals in RDF (and in RDFS and OWL) have two parts: a character string representing the lexical form of the literal, and a datatype name which indicates a function from lexical forms to values. In RDF/S/OWL these two components are incorporated into a special literal syntax; in CL, the datatype is represented as a function name applied to the lexical form as an argument. For example, the RDF literal

"326"^^xsd:integer

would be represented in CL core syntax by the term

(xsd:integer '326')

where the datatype name is used as a function symbol denoting the lexical-to-value mapping corresponding to the datatype. (In practice, the datatypes xsd:integer and xsd:string can often be ignored, as literals typed with these types can be transcribed directly as integers and quoted strings. However, the longer forms can be used if they are found desireable, e.g. to record type information explicitly.)

URIs and RDF graphs

URIs and URI references, the 'bread and butter' of RDF syntax, can be used directly as CL names, so translate transparently into CL. (There are some qualifications in the core syntax: double-quote characters should be escaped, and any URI references which contain a lexical breaking symbol - whitespace, single quote or parentheses - should be rendered in the CL core syntax as a quoted name. See [SCL].) Finally, blank nodes in an RDF graph translate to existentially bound variables with a quantifier whose scope is the entire graph, and of course a graph is the conjunction of the triples it contains.

The translation can then be summarized in the following tables. The rules are understood to apply recursively. Recall that an RDF graph is defined to be a set of triples, while the conjunction into which it translates is a sequence; however, the CL meaning is independent of the ordering, and unchanged by repetition, so the ordering chosen is arbitrary.

The first table is used for all RDF graphs.

The second will be modified when we consider semantic extensions to RDF. Recall that we are here operating under the 'promiscuous' assumption that the RDF and logical universes are the same.

For example, the RDF graph

_:x ex:firstName "Jack"^^xsd:string .
_:x rdf:type ex:Human .
_:x Married _:y .
_:y ex:firstName "Jill"^^xsd:string .

would map into the CL sentence:

(exists (x y)(and
  (ex:firstName x (xsd:string 'Jack'))
  (rdf:type x ex:Human)
  (Married x y)
  (ex:firstName y (xsd:string 'Jill'))
))

The special RDF vocabularies associated with reification, containers and values have no special semantic conditions, so translate uniformly into CL using the above conversion.

RDF Lists

RDF provides a 'collection' vocabulary based on list-processing conventions. Although there is strictly no need to provide axioms for this, it is useful to link it explicitly to one of its major applications, which is to express relations between multiple arguments. Since RDF triple syntax can directly express only unary and binary relations, relations of higher arity must be encoded, and OWL in particular uses lists to do this encoding, so that a relationship betweem four things would be described as a property of a list containing four elements, itself described by a conjunction of binary relationships between those elements and sublists of the list, and between the sublists. This rather awkward process can be summarized in CL by a few basic axioms. These use the CL sequence-variable construction, indicated in CL by the use of the ... ellipsis symbol:

The effect of these axioms is that the atom

(R (list a b ... z))

is equivalent to the 'RDF collection' form, an existentially quantified conjunction:

(exists (l1 l2 ... ln) (and
  (R l1)
  (rdf:first l1 a)
  (rdf:rest l1 l2)
  (rdf:first l2 b)
...
  (rdf:first ln z)
  (rdf:rest ln rdf:nil)
))

We will make use of this in the OWL translations given below, since OWL/RDF uses the RDF list vocabulary extensively.

Perhaps less obviously, the fact that list, first and rest are CL function symbols, which are required to denote total functions on the universe, means that a list containing n items exists just when the items themselves exist. Thus, quantification over lists provides the ability to simultaneously quantify over finite sequences of items. We will also make use of this when writing axioms for the OWL embedding. (The technique used is borrowed from [Fikes&McGuinness].)

RDFS

RDFS is an extension of RDF defined by a number of semantic constraints which impose extra meanings on the RDFS vocabulary, and it gives a special interpretation to rdf:type as being a relationship between a thing and a 'class', which is roughly equivalent in meaning to the set-membership relationship in set theory, often symbolized in mathematics by the epsilon symbol, so that the triple

aaa rdf:type bbb .

corresponds in meaning to

aaa ∈ bbb

which would be naturally rendered in CL as a unary predication

(bbb aaa)

meaning that the property bbb holds of the entity aaa. In this case we also know, from the RDFS semantic conditions, that bbb is an RDFS class. To achieve this extra meaning we add a new RDFS axiom:

where again we adopt a simplifying promiscuity assumption that everything is a class, which will be modified later:

In keeping with the promiscuity assumption, we will also assume that the logical and RDF universes are identical:

Taken together, these axioms justify the more efficient translation table to be used in place of the RDF triple translation table:

where the translations are understood to be carried out in order, with the second used only when the first does not apply. The above example now translates into the more intuitive form

(exists (x y)
  (and
  (ex:firstName x (xsd:string 'Jack'))
  (ex:Human x)
  (Married x y)
  (ex:firstName y (xsd:string 'Jill'))
))

where ex:Human is a genuine predicate.

Similarly to the case for RDF, this assumes that every unary predicate corresponds to an RDFS class; to be more cautious, one would omit the promiscuity axiom and insert an extra assumption explictly as part of the translation process:

In the RDFS semantic specification [RDF-Semantics] several of the constraints are expressed as RDFS assertions ("axiomatic triples") but others are too complex to be represented in RDFS and so must be stated explicitly as external model-theoretic constraints on RDFS interpretations. All of these can be expressed directly as CL axioms, however, so a CL encoding of RDFS is obtained simply by following the translation rules and adding a larger set of axioms. Since the mapping between translated and embedded triples is so close for RDF and RDFS, we use the translated forms of the atomic sentences in stating the axioms needed for the embedding.

RDFS interpretations of a graph can be identified with CL interpretations of the translation of the graph with the RDF and RDFS axioms added.

The atomic sentences in the first table are simply the RDFS axiomatic triples translated into CL using the RDFS translation table (with one small improvement for the domain and range of containerMembershipProperties, where CL can quantify but RDFS had to make an infinite series of atomic assumptions).

The remaining axioms express the "RDFS semantic conditions" [RDF-Semantics] directly in CL.

As noted in the RDF semantics document, it is often appropriate to identify the subclass and subproperty relations with logical quantifier patterns, yielding an 'extensional' semantics. This can be achieved essentially by strengthening several of the implications in the above axioms to biconditionals, but it can also be handled directly:

Note that in this case the axioms for domain, range, subclass and subproperty can all be viewed simply as definitions, and so can be incorporated directly into a translation. The resulting translation table can be thought of as a preamble to the RDF logical form translation:

This exactly captures the 'standard' translation of these terms into conventional first-order logic. In this case the only semantic condition axioms needed are those concerning rdfs:Datatype and rdfs:ContainerMembershipProperty, since the content of the other axioms have been incorporated in to the translation process. Note that it is not required to use these translations: the same results can be derived in CL from the embedding and the axioms; the embedding and translation of extensional RDFS are logically equivalent in CL. However, in practice it may be more efficient to translate directly than to derive the translations from the embedding using CL reasoning.

These extensional translations are the preferred mode for translating the RDFS vocabulary in an OWL context; however, we caution that these extensional translations are not strictly correct for RDFS use, as they embody extensional assumptions which are not RDFS valid.

RDF Datatypes

Datatyped literals have special semantic conditions attached to them: they are required to denote in a 'fixed' way which is determined by an external specification. Unfortunately, the semantic clarity of the datatype theory elucidated in the RDF and OWL semantics documents, in which a single lexical-to-value mapping is assumed to fix the meaning of each datatype, is not always mirrored by the external specifications. The XML Schema specification [XSD], in particular, gives no such clear extensional semantic meaning for the XML Schema family of datatypes, but instead defines a complex set of conditions in which identity of datatype elements is determined contextually by 'facets'; and the notion of 'datatype value' is not used. It is therefore not always strightforward to relate the XSD specifications with the RDF/OWL specifications.

The natural way to specify datatypes in CL is by means of axioms, rather than by model-theoretic specifications. The actual denotation of a typed literal is of little practical importance: what matters is what one can infer about it. For each datatype, we need to be able to recognize several things about any string: when it is a legal lexical form for the datatype, and for any two legal strings, when they are 'the same' according to the datatype rules. For example, the strings '00123' and '123' are 'the same' when viewed by the datatype xsd:number but not 'the same' when viewed by xsd:string. A datatype theory axiomatizes this information directly, using the datatype name both as a predicate indicating the class of legal values and also as a function. CL allows such 'punning', which also follows the RDF practice.

SCL axiom sets can be countably infinite, and it is standard practice to treat any recursively enumerable set of axioms as being a logical theory. Following this standard practice, we can think of a datatype theory as three countably infinite sets of axioms which specify, for all possible strings, which of the are and which are not legal forms, and of the legal forms, which of them are equal to others. For example, the datatype theory for xsd:integer is the infinite conjunction of the following sets of sentences:

(xsd:integer (xsd:integer '0'))
(xsd:integer (xsd:integer '00'))
...
(xsd:integer (xsd:integer '234'))
...

one for every legal numeral string (including those with leading zeros);

(not (xsd:integer (xsd:integer 'a'))
(not (xsd:integer (xsd:integer 'ab'))
...

one for every string which is not a numeral, and

(= (xsd:integer '00')(xsd:integer '0'))
(=(xsd:integer '01')(xsd:integer '1')
...

one for every pair of numerals denoting the same number in which the second has no leading zeros and the first does; the set of all negations of false equations between different integers;

(not (= (xsd:integer '0')(xsd:integer '1'))) ...

and the single axiom

(rdfs:Datatype xsd:integer)

Any similar set of axioms will be called a datatype theory, and the basic CL datatype asumption is that each datatype is somehow associated with a recursively enumerable datatype theory. Of course, in practice this will usually be implemented as an algorithm which, given any atomic sentence of the required form, is able to compute its truth-value; but conceptually we can think of the meaning of a datatype as consisting of a datatype theory. Note that this theory determines the truth value of the expression (xsd:integer (xsd:integer 'string'))for every possible string, and fixes all identities between any two xsd:integer terms; this is the basic requirement of a datatype theory.

Some datatypes theories can be fully axiomatized in a finite number of CL sentences. In particular, the trivial datatype xsd:string is completely captured by the axioms:

(forall (x) (iff (xsd:string (xsd:string x)) (scl:string x) ))
(forall ((x CL:string)) (= x (xsd:string x)))

To achieve the full RDFS meaning of datatypes, we also need an axiom which applies for any datatype and relates typed literals to the general category of rdfs:Literal:

from which it follows that an 'ill-formed' typed literal (where the literal string is not a legal lexical form for the specified datatype) is not in the rdfs:Literal category.

Another (optional) axiom expresses the idea that every literal value must be representable by some literal string, so that there are no 'invisible' values. This was debated in the RDF working group but was not resolved, as no RDF test cases could be found to resolve it. CL is expressive enough to represent the assumption directly:

Note that if this axiom were skolemized, the skolem function would denote the inverse of the lexical-to-value mapping for the datatype x, so that the axiom could be taken to be an assertion that this mapping is always invertible. Note also that this axiom asserts that the string exists, but does not of course enable the relevant string to be computed.

As with the collection vocabulary, the use of this datatype convention means that the universe of discourse is required to contain many entities, since the datatype function symbols must denote total functions.

CL arithmetic

Common Logic treats decimal numerals as a 'datatyped' category which are required to denote their numerical values. We can think of a numeral such as 345 in CL as being an abbreviation of the datatyped term using xsd:integer applied to the numeral string:

(= 345 (xsd:integer '345'))

with the corresponding set of datatyped axioms. (It is not possible to express the general form of this in CL since there is no way to quantify into CL quoted strings. A future version of CL may provide this functionality.) This alone does not provide any arithmetic functionality in CL, but we will assume in addition that the operations of addition and multiplication, and the numerical ordering relationship are defined on numerals as CL functions plus and times and the binary relations lesseq and less. We can consider this to be an infinite set of axioms analagous to a datatype theory, consisting of all the true equations of the form

(= (plus [n] [m]) [n+m])

for decimal numerals [n] and [m], such as (= (plus 32 58) 90)Notice that the negations of any false equations follow from this together with the datatype theory. The axioms for less then use tail recursion in the obvious way:

(forall ((x number))(not(less x 0)))
(forall ((x number)(y number))(and
  (iff (less x (plus y 1))(or (= x y)(less x y)))
  (iff (lesseq x y)(or (= x y)(less x y)))
))

(All that is strictly necessary is an infinite set of axioms defining the successor function:

(= (1 (suc 0)) (= (2 (suc 1)) ...

since the other functions and relations can then be defined by tail-recursion on suc, providing an axiomatic connection between decimal and unary arithmetic. However, it is obviously more convenient to assume decimal notation as a given. An axiom such as

(and (= plus +) (= times .)(= less <)

is sufficient to establish conventional abbreviations, if required. Note however the the symbol '<' must be escaped in XML text.)

OWL

OWL is two (or three) closely related dialects, which share a common set of basic definitions but differ in scope and by the degree to which their syntactic forms are restricted. OWL-Full is the least encumbered of the three, and the closest to RDFS; OWL-DL can be processed by efficient description logic search engines and hence is probably the most widely used dialect; and OWL-Lite is a subset of OWL-DL which omits certain features so as to produce a 'frame-like' language.

The differences between these dialects arise from a clash of priorities. The basic design of OWL is a description logic, but part of its design specification was that it should be an extension to the RDF language family, and to be rendered using RDF triples syntax. Fitting these requirements together was not easy, and requires some ad-hoc constructions to be used which are not particularly well motivated by the intended semantics. The working group tasked with the design of OWL was therefore faced with a conflict of priorities, and the dialects reflect this conflict. OWL-DL cleaves as closely as possible to the classical description logic structure and semantics, and in fact is based upon an 'abstract syntax' [OWLsemanticsPart2] which bears no particular relationship to RDF. Seen from the DL perspective, the choice of primitives for the OWL/RDF syntax is somewhat arbitrary and ad-hoc, and of secondary importance. OWL-Full, in contrast, takes the RDF/RDFS framework as basic and makes the fewest changes to it compatible with the OWL semantics. This takes it beyond the boundaries of the classical description logic translation in various ways.

All dialects of OWL impose the 'extensional' meanings of the RDFS vocabulary, so we will assume that we are using the extensional ("iff") versions of the RDFS semantic condition axioms.

Wild OWL

We will use the term 'wild OWL' to refer to the language obtained by allowing the free use of the OWL vocabulary in RDF syntax, with no restrictions placed on its use. It assumes that the RDF, OWL and logical universes are identical, uses the OWL primitives as far as possible as a semantic extension to RDF and RDFS, and ignores the elaborate sorting introduced in order to protect the constraints needed by OWL-DL and OWL-Lite; in particular, it makes no distinction between datatype values and other entities. This is therefore not, strictly, a legal strategy for any official version of OWL - it permits, for example, the application of inverseFunctionalProperty to datatype properties, and 'mixed' oneOf classes which contain both individuals and datatype values - but is included here as a basis for the later, more complex, translations; because of its logical simplicity; and to illustrate how straightforward it is to express the OWL intuitions directly in CL. The 'official' translations, given later, for OWL-Full and OWL-DL will be based on this, and use many of the same constructions, but will have extra complexities introduced in order to handle the peculiarities of the OWL design.

RDF and RDFS are so simple that the embedding and translation are equivalent. OWL is sufficiently complex that the two styles begin to diverge significantly, so we first give a translation, then discuss how one could describe OWL axiomatically in CL based on the OWL/RDF triple embedding. Some aspects of OWL are best handled by axioms even when translating, however.

We will assume the axioms stated so far (including the optional extensional RDFS axioms) but we add the following axioms in addition to those already described.

Following our promiscuous strategy, we identify the OWL and logical universes, so that owl:Thing and rdfs:Resource both identify the same universe, rendering the quantifier restrictions temporarily vacuous. This will be retracted later when we consider domesticated versions of OWL.

Note that with the earlier promiscuity assumptions, this means that in this translation, every owl:Thing is also an rdf:Property and an rdfs:Class; we emphasize again that this is not a legal assumption for any official OWL dialect.

Translating Wild OWL into CL

To use the table below to translate an OWL/RDF graph, simply generate the corresponding CL for every subgraph of G which matches the pattern specified in the left-hand column. The notation ALLDIFFERENT is used as a shorthand for conjunction of n(n-1) inequations which assert that the terms are all distinct:

[ALLDIFFERENT x1 ... xn]

means

(and
(not (= x1 x2)) (not (=x1 x3)) ... (not (= x1 xn))
(not (= x2 x3)) ... (not (= x2 xn))
(not (= x3 xn)) ...
...
(not (= xn-1 xn))
)

Unlike the RDFS translation, this translates entire RDF subgraphs into logical sentences. To achieve a full translation, all matching subgraphs must be translated, and then any remaining triples rendered into logical atoms using the RDF translation. Note that a triple in the graph may occur in more than one subgraph; in particular, the owl:onProperty triples will often occur in several subgraph patterns when cardinality and value restrictions are used together.

Embedding Wild OWL into CL

To achieve the same effect by using CL axioms to connect the embedded triples to their meaning involves the use of some auxiliary logical machinery. Some of the translations can be mirrored directly by 'iff' statements making the connection directly, as with the RDFS extensional meanings:

Some OWL constructions use lists of arguments expressed using the RDF collection vocabulary. Assuming earlier translations and axioms, these are equivalent to the (list ...) construction. We translate these using auxiliary relations which have their own defining axioms, given below. These all use the same 'recursive' style described in [SCL], where two axioms are given: one for the 'empty sequence' or null case, and the other which defines the meaning of a sequence construction containing at least one element in terms of the immediate subsequence gotten by removing that element. The general technique should be familiar to anyone acquainted with recursive programming or logic programming. Reasoning with these constructions amounts in practice to the use of tail-recusion added to normal first-order expressivity, a technique pioneered by KIF [KIF]. The owl:AllDifferent construction involves a double recursion to generates n(n-1) inequalities for a list of n arguments. Note that the ALLDIFFERENT abbreviation convention used in the translation table has now become a genuine CL expression, which could in fact be used in the translation, if supplemented with its defining axioms.

The OWL value restrictions can be described directly by axioms. These refer to the RDF encoding of OWL, in which the connection between a restriction on a property to the property itself is expressed by a triple with the predicate owl:onProperty.

The cardinality restrictions require the use of nested quantifier sequences whose length depends on the integer used in the restriction. To axiomatize this requires the use of auxiliary axioms involving lists. The axiomatic technique used here is copied directly from [Fikes&McGuinness], and the same terminology is used. The key semantic property on which these rely was noted earlier: in any CL intepretation which satisfies the list axioms, a list of n items exists just when the n items exist as individuals. Thus, quantifying over lists with n items is exactly equivalent in meaning to writing n nested quantifiers over individuals; establishing the existence of such a list establishes the existence of n individuals.

First we list the new 'auxiliary' axioms needed to express the required properties of lists (most notably, their length, expressed using the CL plus primitive on integers).

Domesticated OWLs: OWL Full and OWL DL

The above translations capture the meaning of OWL text, but they do not reproduce the distinction between individual values and datatype values, with its concomitant distinction between owl:objectProperty and owl:datatypeProperty, which is built into all the OWL dialects, or the strict segregation between classes, properties and individuals which is required by OWL-DL and its subdialect OWL-Lite. As most of these are simply syntactic restrictions rather than changes to the logical content, they are not actually required for the translation in a strict sense: the above translation table will accurately transcribe the logical meaning of any legal OWL text in all three dialects. However, the axioms used should be modified for the various dialects, replacing our promiscuity assumptions by more careful attention to typing, and the 'cautious' assumptions need to be modified, and in some cases handled differently for different contexts.

For ease of reference we summarize the axioms which will need modification:

From now on, these axioms are rejected. In their place we introduce a hierarchy of categories identified by the CL transcriptions of the RDF/RDFS/OWL system of class names (together with owl_Property, which plays the role of the union of owl:DatatypeProperty and owl:ObjectProperty), which we assume to be arranged in a hierarchy expressed by the following axioms. For OWL-Full, assume only those in the first table; for OWL-DL also add those in the second table. The first axiom in the table is a domesticated version of the first OWL identity axiom.

We use the 'cautious' forms of the translation tables, introducing explict typing assumptions as required. (Since OWL-DL syntax requires every name to be given an explicit rdf:type, the additional assumptions in the third column are not strictly needed when translating OWL-DL, since they will be translated from the OWL/RDF syntax in any case; they can also be inferred from the OWL and RDFS domain and range information when required.)

More significantly, all the quantifiers in the translation tables and axioms should be restricted to the appropriate category. For example, the owl:equivalentClass translation sentence:

(forall (c d) (iff
  (owl:equivalentClass c d)
  (forall (x) (iff (c x)(d x))) ))

must now be rewritten to apply only to OWL classes:

(forall ((c owl:Class) (d owl:Class)) (iff
  (owl:equivalentClass c d)
  (forall (x) (iff (c x)(d x))) ))

and so on throughout the entire translation table and axioms. This avoids unwarranted 'back-inference' to an owl:equivalentClass assertion from some universal biconditional holding between two predicates which do not qualify as OWL-DL classes, for some reason – of which there are many. Finally, some of the entries in the translation table need to be modified or split into subcases, since the 'same' meaning is expressed differently in domestic OWL depending on whether one is referring to object or datatype properties.

The final version of the translation table is then as follows.

OWL assertions involving annotation properties and ontology properties are not mentioned in these tables explicitly, so will be simply transcribed as atomic assertions in CL, following the RDF conventions.

Examples

@@@not yet done@@@

References

[RDF-CONCEPTS]

Resource Description Framework (RDF): Concepts and Abstract Syntax, Graham Klyne and Jeremy J. Carroll, Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/ . Latest version available at http://www.w3.org/TR/rdf-concepts/ .

[RDF-SEMANTICS]

RDF Semantics, Patrick Hayes, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-mt-20040210/ . Latest version available at http://www.w3.org/TR/rdf-mt/ .

[RDF-TESTCASES]

RDF Test Cases, Jan Grant and Dave Beckett, Editors, W3C Recommendation, 10 February 2004

[RDF-SYNTAX]

RDF/XML Syntax Specification (Revised), Dave Beckett, Editor, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-syntax-grammar-20040210/ . Latest version available at http://www.w3.org/TR/rdf-syntax-grammar/ .

[XSD]

XML Schema Part 2: Datatypes, Biron, P. V., Malhotra, A. (Editors) World Wide Web Consortium Recommendation, 2 May 2001

[KIF]

Knowledge Interchange Format, Michael R. Genesereth et. al., 1998 (draft American National Standard).

[LBASE]

Lbase: Semantics for Languages of the Semantic Web, Guha, R. V., Hayes, P., W3C Note, 10 October 2003.

[Fikes&McGuinness]

An Axiomatic Semantics for RDF, RDF Schema and DAML+OIL, Fikes, R., McGuinness, D. L., KSL Technical Report KSL-01-01, August 2001.

[RDFS]

RDF Vocabulary Description Language 1.0: RDF Schema, Brickley, D., and Guha, R.V., Editors, W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-schema-20040210/ . Latest version available at http://www.w3.org/TR/rdf-schema/ .

[Webont]

Web Ontology Working Group home page.

[OWL Direct Semantics]

OWL Web Ontology Language Semantics and Abstract Syntax. Section 5: RDF-Compatible Model-Theoretic Semantics, Patel-Schneider, P., Hayes, P., Horrocks, I., (eds), W3C Recommendation, 10 February 2004.

[SCL]

Simple Common Logic, Hayes. P. et al. 2004

[CL]

Common Logic (CL) - A Framework for a Family of Logic-Based Languages. ISO/JTC 1/SC 32N1330 Committee Draft ISO/IEC CD, 2005