The three SWeb languages so far given W3C 'recommendation' status (RDF, RDFS and OWL) can all be translated straightforwardly into SCL. The translations follow a number of standard conventions: classes map into unary relations, properties into binary relations, and expression forms in OWL and RDFS typically 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 [ref RDFSemantics]) also require adding axioms which describe their semantic assumptions explicitly; this is along the lines suggested for 'Lbase' in the 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 SCL 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 SCL syntax using the conventions in the table. The SCL core syntax [SCLcore] and the N-triples notation for RDF [NTriples] are used throughout.

RDF

RDF Triples: the two translation styles

There are two recognized styles for translating RDF into logic. One (as used for example in [Fikes+al]) is transparent and direct; it simply maps all RDF triples into atoms which use a 3-argument 'rdf triple' relation with the triple arguments listed in order. This of course does not in itself establish any logical meaning for these atoms, which must then be provided by axioms. The other style (as used for example in [Lbase]) maps the RDF triple into a logical sentence which captures as far as possible the logical meaning of the triple. A simple RDF triple s p o translates into (rdf_triple s p o) in the first style, but into (p s o) in the second. We will refer to these styles respectively as the 'triple' style and the 'logical form' style. The logical form style used in SCL, accurately reproduces the semantics of RDF.

The choice of one translation rather than the other has produced some controversy, as they result in incompatible translations in a conventional first-order logical syntax, and moreover the logical form 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; for this reason, the triple style is often thought of as the 'standard' style, even though it does not exhibit the natural logical structure. In SCL however they are both fully adequate, fully correct, completely compatible, and further the relationship between them can be expressed axiomatically in the language, by a sentence which we will adopt here as axiomatic:

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

This is based on the premis that all binary relations have the status of RDF properties; and since in SCL 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 SCL 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.

One could rationally deny this, 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, denying the promiscuity assumption. If this is considered desirable then the RDF property axiom could be qualified:

and in this case, in order to maintain the strict equivalence between the styles, the logical form translation would have to introduce the explicit assertion (rdf:Property ppp) as an additional axiom in the translation:

Until further notice we will assume promiscuity in order to keep the translations simpler, but it is straightforward (though tiresome) to introduce the explicit qualifications needed to restrict the RDFS and/or the OWL universes to a subset of the logical universe, by suitably restricting the universal quantifiers where needed. This amounts to representing RDF/RDFS/OWL meta-information as annotations to the logical form. 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. In fact, these represent consequences of the RDF graph which are RDF-valid but which are not captured by the logical form translation, which 'loses' the RDF meta-information during the translation; and so when the 'universal' axiom expressing promiscuity is omitted, such assumptions must be added during the translation on a case-by-case basis.

RDF Literals

Literals in RDF are of two types: plain literals and typed literals. Plain literals translate into SCL quoted strings, possibly paired with a language tag, and in both RDF and SCL 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 SCL 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 SCL, 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 SCL 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 SCL names, so translate transparently into SCL. (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 SCL 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 SCL meaning is independent of the ordering, and unchanged by repetition, so the ordering chosen is arbitrary.

The first table is fixed 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 SCL 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 SCL 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 SCL by a few basic axioms. These use the SCL sequence-variable construction, indicated by the use of the ... ellipsis sign:

The effect of these axioms is that if we know that R is in the category of ListArgRelations, then the atom
(R a b ... z)
is exactly equivalent in meaning to the atom
(R (list a b ... z))
which in turn 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.

Semantic note: the use of the RDF list vocabulary implies that the universe of discourse contains many list entities, since function symbols in SCL must denote total functions.

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 SCL 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:

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

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 less promiscuous and more cautious, one would omit the promiscuity axiom, modify the first axiom and insert an extra assumption explictly as part of the translation process:

In the RDFS semantic specification [refRDFS] 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 SCL axioms, however, so the SCL encoding of RDFS is obtained simply by following the translation rules and adding a larger set of axioms. RDFS interpretations of a graph can be identified with SCL 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 SCL using the RDFS logical form translation table (with one small improvement for the domain and range of containerMembershipProperties, where SCL can quantify but RDFS had to make an infinite series of atomic assumptions) .

The remaining axioms express the "RDFS semantic conditions" [RDFSemantics] directly in SCL.

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

This can be used to render several of the above RDFS axioms trivial and simplifies others, but we leave them in this form to emphasise their corespondence to the RDFS semantic conditions and so that the RDFS axioms retain their meaning when we limit the promiscuity assumptions later.

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 the 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. Note that it is not required to use these translations: the same results can be derived in SCL from the translation obtained from any version of the simple RDF translation tables and our axioms. However, in practice it may be more efficient to translate directly than to derive the translations using SCL 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 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 XSD 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 SCL 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. SCL 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; and the single axiom

(rdfs:Datatype xsd:integer)

Any similar set of axioms will be called a datatype theory, and the basic SCL 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; this is the basic requirement of a datatype theory.

Some datatypes theories can be fully axiomatized in a finite number of SCL 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 scl: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. SCL is expressive enough to represent the assumption directly:

Note that if this axiom were skolemized, the skolem function would denote an 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.

OWL

OWL is two (or three) closely related dialects rather than a single language, 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. It is natural to

Although any of these dialects can be translated into SCL in either of the two styles already used, it is natural to use the triple translation style for OWL-Full, applied directly to the OWL/RDF syntax, and the logical-form translation style for OWL-DL, applied to the abstract syntax. As with RDF and RDFS, the relationships between the two styles can be expressed directly in SCL axioms, allowing them to be intermixed and to be translated into one another.

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, and will follow the technique used there of mapping OWL constructions directly into SCL sentences, extending the RDF translation table, rather than defining the meaning of a bare RDF literal translation by means of axioms. (The axiomatic approach is straightforward for all of OWL except for the cardinality restrictions, where the SCL translation depends on the numerical value of the cardinality specification. To describe this construction axiomatically is theoretically possible in SCL, which allows a form of tail-recursion, but would be extremely opaque and almost certainly produce an inefficient translation process. The general technique of handling tail-recursion is illustrated by the treatment of RDF lists.)

Wild OWL

This translation stays even closer to the RDF/RDFS view of the world than OWL-Full. 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; in particular, it makes no distinction betwen datatype values and other entities. This is therefore not, strictly, a legal set of axioms for any official version of OWL - it permits, for example, the application of inverseFunctionalProperty to datatype properties, and 'mixed' oneOf classes which contian both individuals and datatype values - but is included here to illustrate how straightfoward it would have been to express the OWL intuitions directly in SCL. 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.

The RDFS translation rules apply, and we assume the axioms stated so far (including the optional extensional RDFS axioms) but we add the following axioms in addition to those already described. All of these axioms use iff to connect OWL constructions with their 'logical' meanings. Such two-way connections establish many implications between pieces of the OWL vocabulary which are of doubtful utility in practice, and greatly complicate the search for valid inferences. Later we consider a weaker translation using implication which corresponds to the use of OWL constructions as 'rules', and is sufficient for most practical applications of OWL to instance data.

Following our promiscuous strategy, we identify the OWL and logical universes, so that owl:Thing and rdfs:Resource both identify the same universe. Note that with out 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.

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. Reasoning with these constructions amounts in practice to the use of tail-recusion added to normal first-order expressivity, a technique pioneered by KIF [refKIF]. The owl:AllDifferent construction involves a double recursion to generates n(n-1) inequalities for a list of n arguments.

The axioms which describe the meanings of the auxiliary syntax 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 list construction containing at least one element in terms of the immediate 'tail' sublist gotten by removing that element. In each case, the meaning of the construction is given by using an auxiliary function from lists to unary relations, a construction which is illegal in conventional first-order syntax but legal (and indeed conventional) in SCL. These all utilize the (list ...) convention which is defined by the RDF List axioms and related to the RDF collection vocabulary by the RDF List Argument axiom. Reasoning with these constructions amounts in practice to the use of tail-recusion added to normal first-order expressivity, a technique pioneered by KIF [refKIF]. The owl:AllDifferent construction involves a double recursion to generate n(n-1) inequalities for a list of n arguments. Unwrapping these recursions makes

(ALLDIFFERENT x1 ... xn)

translate into

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

The OWL restrictions are coded into RDF triples using an auxiliary RDF property owl:onProperty which relates the restriction class to the property used to define it. Assuming that the triples containing this property are translated into SCL atomic sentences, the meanings of the OWL value restrictions can be described by axioms.

As mentioned, the cardinality restrictions require the use of nested quantifier sequences, which makes it more convenient to translate them using an extended translation table which maps subgraphs of the RDF graph into the corresponding logical forms. Note that (in contrast to the RDFS triple translation table) this is intended to be applied in addition to the other translations. For example, the owl:onProperty triples will also produce the atoms which play the role of antecedents in the above axioms. These translations also make use of the recursively defined auxiliary functions defined earlier.

This translation completely reproduces the OWL meaings in SCL, and does so by as far as possible reproducing the OWL/RDF exactly in SCL and then using SCL axioms to specify their meaning. As with RDFS, if one is willing to accept a translation which ignores the 'structural' implications between pieces of the OWL vocabulary, and simply reproduces the logical meanings of the OWL in SCL directly, then the entire translation can be specified more simply by an extended translation table, using far fewer axioms.

To use this table to translate an OWL/RDF graph, simply generate the corresponding SCL for every subgraph of G which matches the pattern specified in the left-hand column. In this case we simply transcribe RDF lists directly into SCL argument sequences, dispensing with the left-recursive auxiliary functions. The ALLDIFFERENT is used here for brevity, but should here be understood as a shorthand for the sets of inequations specified by the above-noted equivalence. Note that the negation of an ALLDIFFERENT is a disjunction of equations.

Wih this translation table, the only axioms required are the OWL identity axioms and the earlier RDF and RDFS axioms.

OWL Full and OWL DL

These 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 much stricter segregation between classes and individuals which is required by OWL-DL. As most of these are simply encoding 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 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.

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

@@@not yet finished@@@