index.html 68 KB

Raw Blame History Permalink

<?xml version="1.0" encoding="iso-8859-1"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">

<html xmlns="http://www.w3.org/1999/xhtml">
  <head>
    <meta name="generator"
    content="HTML Tidy for Linux/x86 (vers 1st March 2002), see www.w3.org" />

    <title>LBase: Semantics for Languages of the Semantic Web</title>
    <meta http-equiv="Content-Type"
    content="text/html; charset=iso-8859-1" />
<style type="text/css">
/*<![CDATA[*/

P.c3 { FONT-STYLE: italic}
P.c2 {   FONT-STYLE: italic; TEXT-ALIGN: center}
P.c1 {   TEXT-ALIGN: center}
.new {   }
.newer {   }
.cream {   BACKGROUND-COLOR: #ffff99}
.lilac {   BACKGROUND-COLOR: #ff99ff}
.datatype  {   FONT-SIZE: small;
    FONT-FAMILY: monospace;
    BACKGROUND-COLOR: #99cc99
}

 div.c1 {text-align: center}

/*]]>*/
</style>
    <link rel="stylesheet" type="text/css"
    href="http://www.w3.org/StyleSheets/TR/W3C-WG-NOTE.css" />
  </head>

  <body lang="en">
    <div class="head">
      <a href="http://www.w3.org/"><img height="48" width="72"
      alt="W3C" src="http://www.w3.org/Icons/w3c_home" /></a>

      <h1 id="title">LBase: Semantics for Languages of the Semantic Web</h1>


      <h2 id="w3c-note">W3C Working Group Note 10 October 2003</h2>

      <dl>
        <dt>This version:</dt>


    <dd><a
        href="http://www.w3.org/TR/2003/NOTE-lbase-20031010/">http://www.w3.org/TR/2003/NOTE-lbase-20031010/</a></dd>

        <dt>Latest version:</dt>

        <dd><a
        href="http://www.w3.org/TR/lbase">http://www.w3.org/TR/lbase</a></dd>

		<dt>Previous version:</dt>

		<dd><a href="http://www.w3.org/TR/2003/NOTE-lbase-20030905">http://www.w3.org/TR/2003/NOTE-lbase-20030905</a></dd>

        <dt>Authors:</dt>

        <dd>R.V.Guha, IBM, &lt; <a
        href="mailto:rguha@us.ibm.com">rguha@us.ibm.com</a>&gt;</dd>


    <dd><a href="http://www.coginst.uwf.edu/%7Ephayes/">Patrick Hayes</a>, IHMC
      &lt; <a
        href="mailto:phayes@ihmc.us">phayes@ihmc.us</a>&gt;</dd>
      </dl>

      <p class="copyright"><a
      href="http://www.w3.org/Consortium/Legal/ipr-notice#Copyright">Copyright</a>
      &copy; 2003 <a href="http://www.w3.org/"><acronym
      title="World Wide Web Consortium">W3C</acronym></a><sup>&reg;</sup>
      (<a href="http://www.lcs.mit.edu/"><acronym
      title="Massachusetts Institute of Technology">MIT</acronym></a>,
      <a href="http://www.ercim.org/"><acronym
      title="European Research Consortium for Informatics and Mathematics">
      ERCIM</acronym></a>, <a href="http://www.keio.ac.jp/">Keio</a>),
      All Rights Reserved. W3C <a
      href="http://www.w3.org/Consortium/Legal/ipr-notice#Legal_Disclaimer">
      liability</a>, <a
      href="http://www.w3.org/Consortium/Legal/ipr-notice#W3C_Trademarks">
      trademark</a>, <a
      href="http://www.w3.org/Consortium/Legal/copyright-documents">document
      use</a> and <a
      href="http://www.w3.org/Consortium/Legal/copyright-software">software
      licensing</a> rules apply.</p>
    </div>
    <hr />

    <h2 id="abstract">Abstract</h2>

    <p>This document presents a framework for specifying the semantics
    for the languages of the Semantic Web. Some of these languages
    (notably RDF [<a href="#ref-rdf-primer">RDF-PRIMER</a>] [<a
    href="#ref-rdf-schema">RDF-VOCABULARY</a>] [<a
    href="#ref-rdf-syntax">RDF-SYNTAX</a>] [<a
    href="#ref-rdf-concepts">RDF-CONCEPTS</a>] [<a
    href="#ref-rdf-semantics">RDF-SEMANTICS</a>], and OWL [<a
    href="#ref-owl">OWL</a>]) are currently in various stages of
    development and we expect others to be developed in the future.
    This framework is intended to provide a framework for specifying
    the semantics of all of these languages in a uniform and coherent
    way. The strategy is to translate the various languages into a
    common 'base' language thereby providing them with a single
    coherent model theory.</p>

    <p>We describe a mechanism for providing a precise semantics for
    the Semantic Web Languages (referred to as SWELs from now on. The
    purpose of this is to define clearly the consequences and allowed
    inferences from constructs in these languages.</p>

    <h2 class="no-num" id="status">Status of This Document</h2>
<p><em>This section describes the status of this document at the time of its publication. Other
documents may supersede this document. A list of current W3C publications and the latest revision of
this technical report can be found in the <a href="http://www.w3.org/TR/">W3C technical reports
index</a> at http://www.w3.org/TR/.</em></p>

<p>
Publication as a Working Group Note does not imply endorsement by the W3C Membership. This is a
draft document and may be updated, replaced or obsoleted by other documents at any time. It is
inappropriate to cite this document as other than work in progress.
</p>

    <p>This document results from discussions within the <a
    href="http://www.w3.org/2001/sw/RDFCore/">RDF Core Working
    Group</a> concerning the formalization of RDF and RDF-based
    languages. The RDF Core Working Group is part of the <a
    href="http://www.w3.org/2001/sw/Activity">W3C Semantic Web
    Activity</a>. The group's goals and requirements are discussed in
    the <a href="http://www.w3.org/2001/sw/RDFCoreWGCharter">RDF Core
    Working Group charter</a>. These include requirements that...</p>

    <ul>
      <li><em>The RDF Core group must take into account the various
      formalizations of RDF that have been proposed since the
      publication of the RDF Model and Syntax Recommendation. The group
      is encouraged to make use both of formal techniques and
      implementation-led test cases throughout their work.</em></li>

      <li><em>The RDF schema system must provide an extensibility
      mechanism to allow future work (for example on Web Ontology and
      logic-based Rule languages) to provide richer
      facilities.</em></li>
    </ul>

    <p>This document is motivated by these two requirements. It does
    not present an RDF Core WG design for Semantic Web layering.
    Rather, it documents a technique that the RDF Core WG are using in
    our discussions and in the <a href="#ref-rdf-semantics">RDF
    Semantics specification</a>. The RDF Core WG solicit feedback from
    other Working Groups and from the RDF implementor community on the
    wider applicability of this technique.</p>

    <p>Note that the use of the abbreviation "SWEL" in Lbase differs
    from the prior use of "SWeLL" in the <a
    href="http://www.w3.org/2000/01/sw/#daml">MIT/LCS DAML
    project</a>.</p>

    <p>In conformance with <a
    href="http://www.w3.org/Consortium/Process-20010719/#ipr">W3C
    policy</a> requirements, known patent and <acronym
    title="Intellectual Property Rights">IPR</acronym> constraints
    associated with this Note are detailed on the <a
    href="http://www.w3.org/2001/sw/RDFCore/ipr-statements"
    rel="disclosure">RDF Core Working Group Patent Disclosure</a>
    page.</p>

    <p>Review comments on this document are invited and should be sent
    to the public mailing list <a
    href="mailto:www-rdf-comments@w3.org">www-rdf-comments@w3.org</a>.
    An archive of comments is available at <a
    href="http://lists.w3.org/Archives/Public/www-rdf-comments/">http://lists.w3.org/Archives/Public/www-rdf-comments/</a>.</p>

    <p>Discussion of this document is invited on the <a
    href="mailto:www-rdf-logic@w3.org">www-rdf-logic@w3.org</a> list of
    the <a href="http://www.w3.org/RDF/Interest/">RDF Interest
    Group</a> (<a
    href="http://lists.w3.org/Archives/Public/www-rdf-logic/">public
    archives</a>).</p>

    <h2><a id="toc" name="toc">Table of Contents</a></h2>


<ul>
  <li>1 <a href="#intro">Model-theoretic semantics</a></li>
  <li>2 <a href="#outline">Outline of Approach</a></li>
  <li>2.1 <a href="#consistency">Consistency</a></li>
  <li>2.2 <a href="#syntax">L<sub>base</sub> Syntax</a></li>
  <li>2.3 <a href="#interp">Interpretations</a></li>
  <li>2.4 <a href="#axiom_schemas">Axiom Schemas</a></li>
  <li>2.5 <a href="#entail">Entailment</a></li>
  <li>3 <a href="#using">Using L<sub>base</sub></a></li>
  <li>3.1 <a href="#rel">Relation between the two...</a></li>
  <li>4 <a href="#inaq">Inadequacies of</a></li>
  <li>5 <a href="#acks">Acknowledgements</a></li>
  <li>6 <a href="#refs">References</a></li>
  <li>7 <a href="#change">Change Log</a></li>
</ul>


<h2><a id="intro" name="intro">1. Model-theoretic semantics</a></h2>

    <p>A <a href="http://www.xrefer.com/entry/572261">model-theoretic
    semantics</a> for a language assumes that the language refers to a
    'world', and describes the minimal conditions that a world must
    satisfy in order to assign an appropriate meaning for every
    expression in the language. A particular world is called an
    <i>interpretation,</i> so that model theory might be better called
    'interpretation theory'. The idea is to provide a mathematical
    account of the properties that any such interpretation must have,
    making as few assumptions as possible about its actual nature or
    intrinsic structure. Model theory tries to be metaphysically and
    ontologically neutral. It is typically couched in the language of
    set theory simply because that is the normal language of
    mathematics - for example, this semantics assumes that names denote
    things in a <i>set</i> IR called the 'universe' - but the use of
    set-theoretic language here is not supposed to imply that the
    things in the universe are set-theoretic in nature.</p>

    <p>The chief utility of such a semantic theory is not to suggest
    any particular processing model, or to provide any deep analysis of
    the nature of the things being described by the language, but
    rather to provide a technical tool to analyze the semantic
    properties of proposed operations on the language; in particular,
    to provide a way to determine when they preserve meaning. Any
    proposed inference rule, for example, can be checked to see if it
    is valid with respect to a model theory, i.e. if its conclusions
    are always true in any interpretation which makes its antecedents
    true.</p>

    <p>We note that the word 'model' is often used in a rather
    different sense, eg as in 'data model', to refer to a computational
    system or data structures of some kind. To avoid misunderstanding,
    we emphasise that the interpretations referred to in a model theory
    are not, in general, intended to be thought of as things that can
    be computed or manipulated by computers.</p>


<h2><a id="outline" name="outline">2. Outline of Approach</a></h2>

    <p>There will be many Semantic Web languages, most of which will be
    built on top of more basic Semantic Web language(s). It is
    important that this <em>layering</em> be clean and simple, not just
    for human understandability, but also to enable the construction of
    robust semantic web agents that use these languages. The emerging
    current practice is for each of the SWELs to be defined in terms of
    their own model theory, layering it on top of the model theories of
    the languages they are layered upon. While having a model theory is
    clearly desireable, and even essential, for a SWEL, this
    direct-construction approach has several problems. It produces a
    range of model theories, each with its own notion of consequence
    and entailment. It requires expertise in logic to make sure that
    model theories align properly, and model-theoretic alignment does
    not always sit naturally with interoperability requirements.
    Experience to date (particularly with the OWL standard under
    development at the time of writing by the <a
    href="http://www.w3.org/2001/sw/WebOnt/">W3C Webont working
    group)</a> shows that quite difficult problems can arise when
    layering model theories for extensions to the 'basic' RDF layer
    [RDF] of the semantic web. Moreover, this strategy places a very
    high burden on the 'basic' layer, since it is difficult to
    anticipate the semantic demands which will be made by all future
    higher layers, and the expectations of different development and
    user communities may conflict. Further, we believe that a melange
    of model theories will adversely impact developers building agents
    that implement proof systems for these layers, since the proof
    systems will likely be different for each layer, resulting in the
    need to micro-manage small semantic variations for various dialects
    and sub-languages (cf. the distinctions between various dialects of
    OWL).</p>

    <p>In this document, we use an alternative approach to for defining
    the semantics for the different SWELs in a fashion which ensures
    interoperability. We first define a basic language L<sub>base</sub>
    which is expressive enough to state the content of all currently
    proposed web languages, and has a fixed, clear model-theoretic
    semantics. Then, the semantics of each SWEL L<sub>i</sub> is
    defined by specifying how expressions in the L<sub>i</sub> map into
    equivalent expressions in L<sub>base</sub>, and by providing axioms
    written in L<sub>base</sub> which constrain the intended meanings
    of the SWEL special vocabulary. The L<sub>base</sub> meaning of any
    expression in <em>any</em> SWEL language can then be determined by
    mapping it into L<sub>base</sub> and adding the appropriate
    language axioms, if there are any.</p>

    <p>The intended result is that the model theory of L<sub>base</sub>
    is the model theory of <em>all</em> the Semantic Web Languages,
    even though the languages themselves are different. This makes it
    possible to use a single inference mechanism to work on these
    different languages. Although it will possible to exploit
    restrictions on the languages to provide better performance, the
    existence of a reference proof system is likely to be of utility to
    developers. This also allows the meanings of expressions in
    different SWELs to be compared and combined, which is very
    difficult when they all have distinct model theories.</p>

    <p class="new">The idea of providing a semantics for SWELs by
    translating them into logic is not new [see for example
    Marchiolri&amp;Saarela, Fikes&amp;McGuinness] but we plan to adopt
    a somewhat different style than previous 'axiomatic semantics',
    which have usually operated by mapping all RDF triples to instances
    of a single three-place predicate. We propose rather to use the
    logical form of the target language as an explication of the
    intended meaning of the SWEL, rather than simply as an axiomatic
    description of that meaning, so that RDF classes translate to unary
    predicates, RDF properties to binary relations, the relation
    rdf:type translates to application of a predicate to an argument,
    and list-valued properties in OWL or DAML can be translated into
    n-ary or variadic relations. The syntax and semantics of
    L<sub>base</sub> have been designed with this kind of translation
    in mind. It is our intent that the model theory of L<sub>base</sub>
    be used in the spirit of its model theory and not as a programming
    language, i.e., relations in L<sub>i</sub> should correspond to
    relations in L<sub>base</sub>, variables should correspond to
    variables and so on.</p>

    <p class="new">It is important to note that L<sub>base</sub> is not
    being proposed as a SWEL. It is a tool for specifying the semantics
    of different SWELs. The syntax of L<sub>base</sub> described here
    is not intended to be accessible for machine processing; any such
    proposal should be considered to be a proposal for a more
    expressive SWEL.</p>

    <h2><a id="consistency" name="consistency">2.1 Consistency</a></h2>

    <p>By using a well understood logic (i.e., first order logic
    [Enderton]) as the core of L<sub>base</sub>, and providing for
    mutually consistent mappings of different SWELs into
    L<sub>base</sub>, we ensure that the content expressed in several
    SWELs can be combined consistently, avoiding paradoxes and other
    problems. Mapping type/class language into predicate/application
    language also ensures that set-theoretical paradoxes do not arise.
    Although the use of this technique does not in itself guarantee
    that mappings between the syntax of different SWELs will always be
    consistent, it does provide a general framework for detecting and
    identifying potential inconsistencies.</p>

    <p>It is also important that the axioms defining the vocabulary
    items introduced by a SWEL are internally consistent. Although
    first-order logic (and hence L<sub>base</sub>) is only
    semi-decideable, we are confident that it will be routine to
    construct L<sub>base</sub> interpretations which establish the
    relevant consistencies for all the SWELs currently contemplated. In
    the general case, future efforts may have to rely on certifications
    from particular automated theorem provers stating that they weren't
    able to find an inconsistency with certain stated levels of effort.
    The availablity of powerful inference engines for first-order logic
    is of course relevant here.</p>


<h3><a id="lbase" name="lbase">2.1.1 L<sub>base</sub></a></h3>

    <p>In this document, we use <span class="new">a version of</span>
    first order logic with equality as L<sub>base</sub>. This imposes a
    fairly strict monotonic discipline on the language, so that it
    cannot express local default preferences and several other
    commonly-used non-monotonic constructs. <span class="new">We expect
    that as the Semantic Web grows to encompass more and our
    understanding of the Semantic Web improves, we will need to replace
    this L<sub>base</sub> with more expressive logics. However,</span>
    we expect that first order logic will be a proper subset of such
    systems and hence we will be able to smoothly transition to more
    expressive L<sub>base</sub> languages in the future. We note that
    the computational advantages claimed for various sublanguages of
    first-order logic, such as description logics, logical programming
    languages and frame languages, are irrelevant for the purposes of
    using L<sub>base</sub> as a semantic specification language.</p>

    <p>We will use First Order Logic with suitable minor changes to
    account for the use of referring expressions (such as URIs) on the
    Web, and a few simple extensions to improve utility for the
    intended purposes.</p>


<h3><a id="urisandlit" name="urisandlit">2.1.2 Names</a> and variables</h3>
<p>Any first-order logic is based on a set of <i>atomic terms</i>, which are used
  as the basic referring expressions in the syntax. These include <i>names</i>,
  which refer to entities in the domain, <i>special names</i>, and <i>variables</i>.
  L<sub>base</sub> distinguishes the special class of <em>urirefs</em>, defined
  to be a URI reference in the sense of [URI]. Urirefs are used to refer to both
  individuals and relations between the individuals. A name may be any string
  of unicode characters not starting with the characters ')','(', '\', '?','&lt;'
  or ''' , and containing no whitespace characters, or any string of unicode characters
  enclosed by the symbols '&lt;' and '&gt;'. The &lt;-&gt; enclosed style is provided
  to allow names which would otherwise violate the L<sub>base</sub> syntactic
  conventions; in this case it is understood that the actual name is the enclosed
  string. For example, the name '&lt;br /&gt;' (eight characters, including a
  space) can be written in L<sub>base</sub> as &lt;'&lt;br /&gt;'&gt;.</p>
<p>L<sub>base</sub> allows for various collections of special names with fixed
  meanings defined by other specifications (external to the L<sub>base</sub> specification).
  There is no assumption that these could be defined by collections of L<sub>base</sub>
  axioms, so that imposing the intended meanings on these special names may go
  beyond strict first-order expressiveness. (In mathematical terms, we allow that
  some sets of names refer to elements of certain fixed algebras, even when the
  algebra has no characteristic first-order description.) <span class="new">Each
  such set of names has an associated predicate which is true of the things denoted
  by the names in the set.</span> At present, we assume two categories of such
  fixed names: numerals and quoted strings, with associated predicate names 'NatNumber'
  and 'String' respectively. We expect that other categories of special names
  will be introduced to handle, eg. XML structures.</p>

    <p>Numerals are defined to be strings of the characters
    '0123456789', and are interpreted as decimal numerals in the usual
    way. Since arithmetic is not first-order definable, this is the
    first and most obvious place that L<sub>base</sub> goes beyond
    first-order expressiveness.</p>
<p>Quoted strings are arbitrary character sequences enclosed in <span class="new">(single)</span>
  quotation marks, and are interpreted as denoting the string inside the quotation
  marks. To avoid ambiguity, single quote marks in strings are prefixed by a backslash
  character '\' which acts an escape character, so that '\'A\\'' denotes the string
  'A\'. <span class="new">Double quote marks have no special interpretation.</span>
</p>

    <p class="new">The associated predicate names <em>NatNumber</em>, <em>String</em>
  and <em>Relation</em> (see below) are considered to be special names.</p>

    <p>A variable is any non-white-space character string starting with
    the character '?'.</p>

    <p>The characters '(', ',' and ')' are considered to be punctuation
    symbols.</p>

    <p>The categories of punctuation, whitespace, names, special names
    and variables are exclusive and each such string can be classified
    by examining its first character. This is not strictly necessary
    but is a useful convention.</p>

    <p>Any L<sub>base</sub> language is defined with respect to a
    <i>vocabulary</i>, which is a set of non-special names. We require
    that every L<sub>base</sub> vocabulary contain all urirefs, but
    other expressions are allowed. (We will require that every
    L<sub>base</sub> interpretation provide a meaning for every special
    name, but these interpretations are fixed, so special names are not
    counted as part of the vocabulary.)</p>

    <p>There are several aspects of meaning of expressions on the
    semantic web which are not yet treated by this semantics; in
    particular, it treats URIs as simple names, ignoring aspects of
    meaning encoded in particular URI forms [RFC 2396] and does not
    provide any analysis of time-varying data or of changes to URI
    denotations. The model theory also has nothing to say about whether
    an HTTP uri such as "http://www.w3.org/" denotes the World Wide Web
    Consortium or the HTML page accessible at that URI or the web site
    accessible via that URI. These complexities may be addressed in
    future extensions of L<sub>base</sub>; in general, we expect that
    L<sub>base</sub> will be extended both notationally and by adding
    axioms in order to track future standardization efforts.</p>

    <p>We do not take any position here on the way that urirefs may be
    composed from other expressions, e.g. from relative URIs or Qnames;
    the model theory simply assumes that such lexical issues have been
    resolved in some way that is globally coherent, so that a single
    uriref can be taken to have the same meaning wherever it
    occurs.</p>

    <p>Similarly, the model theory given here has no special provision
    for tracking temporal changes. It assumes, implicitly, that urirefs
    have the same meaning <em>whenever</em> they occur. To provide an
    adequate semantics which would be sensitive to temporal changes is
    a research problem which is beyond the scope of this document..</p>

    <h3><a id="syntax" name="syntax">2.2 L<sub>base</sub>
    Syntax</a></h3>
    Even though the exact syntax chosen for L<sub>base</sub> is not
    important, we do need a syntax for the specification. We follow the
    same general conventions used in most standard presentations of
    first-order logic, with one generalization which has proven useful.


    <p>We will assume that there are three sets of names (not special
    names) which together constitute the vocabulary: individual names,
    relation names, and function names, and that each function name has
    an associated <i>arity</i>, which is a non-negative integer. In a
    particular vocabulary these sets may or may not be disjoint.
    Expressions in L<sub>base</sub> (speaking strictly,
    L<sub>base</sub> expressions in this particular vocabulary) are
    then constructed recursively as follows:</p>

    <p>A <i>term</i> is either a name or a special name or a variable,
    or else it has the form f(t1,...,tn) where f is an n-ary function
    name and t1,...,tn are terms.</p>

    <p>A <i>formula</i> is either atomic or boolean or quantified,
    where:</p>

    <p>an atomic formula has the form (t1=t2) where t1 and t2 are
    terms, or else the form R(t1,...,tn) where R is a relation name or
    a variable and t1,...,tn are terms;</p>

    <p>a boolean formula has one of the forms</p>

    <p>(W1 and W2 and ....and Wn)<br />
     (W1 or W2 or ... or Wn)<br />
     (W1 implies W2)<br />
     (W1 iff W2)<br />
     (not W1)</p>

    <p>where W1, ...,Wn are formulae; and</p>

    <p>a quantified formula has one of the forms</p>

    <p>(forall (?v1 ...?vn) W)<br />
     (exist<span class="new">s</span> (?v1 ... ?vn) W)</p>

    <p>where ?v1,...,?vn are variables and W is a formula. (The
    subexpression just after the quantifier is the <em>variable
    list</em> of the quantifier. Any occurrence of a variable in W is
    said to be <em>bound</em> in the quantified formula <em>by</em> the
    nearest quantifer to the occurrence which includes that variable in
    its variable list, if there is one; otherwise it is said to be
    <em>free</em> in the formula.)</p>

    <p>Finally, an L<sub>base</sub> <i>knowledge base</i> is a set of
    formulae.</p>

    <p>Formulae are also called 'wellformed formulae' or 'wffs' or
    simply 'expressions'. In general, surplus brackets may be omitted
    from expressions when no syntactic ambiguity would arise.</p>

    <p>Some comments may be in order. The only parts of this definition
    which are in any way nonstandard are (1) allowing 'special names',
    which was discussed earlier; (2) allowing variables to occur in
    relation position, which might seem to be at odds with the claim
    that L<sub>base</sub> is first-order - we discuss this further
    below - and (3) not assigning a fixed arity to relation names. This
    last is a useful generalization which makes no substantial changes
    to the usual semantic properties of first-order logic, but which
    eases the translation process for some SWEL syntactic constructs.
    (The computational properties of such 'variadic relations' are
    quite complex, but L<sub>base</sub> is not being proposed as a
    language for computational use.)</p>

    <h3><a id="interp" name="interp">2.3 Interpretations &amp;
    Satisfaction</a></h3>

    <p>The following definition of an interpretation is couched in
    mathematical language, but what it amounts to intuitively is that
    an interpretation provides just enough information about a possible
    way the world might be - a 'possible world' - in order to fix the
    truth-value (true or false) of any L<sub>base</sub> well formed
    formula in that world. It does this by specifying for each uriref,
    what it is supposed to be a name of; and also, if it is a function
    symbol, what values the function has for each choice of arguments;
    and further, if it is a relation symbol, which sequences of things
    the relation holds between. This is just enough information to
    determine the truth-values of all atomic formulas; and then this,
    together with a set of recursive rules, is enough to assign a truth
    value for any L<sub>base</sub> formula.</p>

    <p>In specifying the following it is convenient to define use some
    standard definitions. A relation over a set S is a set of finite
    sequences (tuples) of members of S. If R is a relation and all the
    elements of R have the same length n, then R is said to have
    <i>arity</i> n, or to be a <i>n-ary relation</i>. Not every
    relation need have an arity. If R is an (n+1)-ary relation over S
    which has the property that for any sequence &lt;s1,...,sn&gt; of
    members of S, there is exactly one element of R of the form &lt;s0,
    s1, ..., sn&gt;, then R is an n-ary <i>function</i>; and s0 is the
    <i>value</i> of the function for the arguments s1, ...sn. (Note
    that an n-ary function is an (n+1)-ary relation, and that, by
    convention, the function value is the first argument of the
    relation, so that for any n-ary function f, f(y,x1,...,xn) means
    the same as y = f(x1,...,xn).)</p>

    <p>The conventional textbook treatment of first-order
    interpretations assumes that relation symbols denote relations. We
    will modify this slightly to require that relation symbols denote
    entities with an associated relation, called the relational
    extension, and will sometimes abuse terminology by referring to the
    entities with relational extensions as relations. This device gives
    L<sub>base</sub> some of the freedom to quantify over relations
    which would be familiar in a higher-order logic, while remaining
    strictly a first-order language in its semantic and metatheoretic
    properties. <span class="new">We will use the special name
    <em>Relation</em> to denote the property of having a relational
    extension.</span></p>

    <p>Let VV be the set of all variables, and NN be the set of all
    special names.</p>


<p>We will assume that there is a globally <em>fixed</em> mapping SN from elements
  of NN to a domain ISN (i.e, consisting of character strings and integers). The
  exact specification of SN is given for numerals by the usual reading of a decimal
  numeral to denote a natural number and for quoted strings by the dequotation
  rules described earlier.</p>

    <p>An <em>interpretation</em> I of a vocabulary V is then a
    structure defined by:</p>

    <ul>
      <li>a set ID, called the domain or universe of I;</li>

      <li>a mapping IS from (V union VV) into ID;</li>

      <li>a mapping IEXT from IR, a subset of ID, into a relation over
      <span class="new">ID+ISN (ie a set of tuples of elements of
      ID+ISN).</span></li>
    </ul>

    <p>which satisfies the following conditions:</p>


<ul class="noindent">
  <li class="new">for any n-ary function symbol f in V, IEXT(I(f)) is an n-ary
    function over ID+ISN.</li>
  <li class="new">IEXT(I(<em>NatNum</em>)) = {&lt;n&gt;, n a natural number}</li>
  <li class="new">IEXT(I(<em>String</em>)) = {&lt;s&gt;, s a character string}</li>
  <li class="new">IEXT(I(<em>Relation</em>)) = IR</li>
</ul>

    <p>An interpretation then specifies the value of any other
    L<sub>base</sub> expression E according to the following rules:</p>

    <table width="90%" border="1" summary="rules">
      <!--DWLayoutTable-->

      <tbody>
        <tr>
          <td width="39%"><strong>if E is:</strong></td>

          <td width="61%"><strong>then I(E) is:</strong></td>
        </tr>

        <tr>
          <td width="39%">a name or a variable</td>

          <td width="61%">IS(E)</td>
        </tr>

        <tr>
          <td width="39%">a special name</td>

          <td width="61%">SN(E)</td>
        </tr>

        <tr>
          <td width="39%">a term f(t1,...,tn)</td>

          <td width="61%">the value of IEXT(I(f)) for the arguments
          I(t1),...,I(tn)</td>
        </tr>

        <tr>
          <td width="39%">an equation (A=B)</td>

          <td width="61%">true if I(A)=I(B), otherwise false</td>
        </tr>

        <tr>
          <td width="39%">a formula of the form R(t1,...,t2)</td>

          <td width="61%">true if IEXT(I(R)) contains the sequence
          &lt;I(t1),...,I(tn)&gt;, otherwise false</td>
        </tr>

        <tr>
          <td width="39%">(W1 and ...and Wn)</td>

          <td width="61%">true if I(Wi)=true for i=1 through n,
          otherwise false</td>
        </tr>

        <tr>
          <td width="39%">(W1 or ...or Wn)</td>

          <td width="61%">false if I(Wi)=false for i=1 through n,
          otherwise true</td>
        </tr>

        <tr>
          <td width="39%">(W1 &lt;=&gt; W2)</td>

          <td width="61%">true if I(W1)=I(W2), otherwise false</td>
        </tr>

        <tr>
          <td width="39%">(W1 =&gt; W2)</td>

          <td width="61%">false if I(W1)=true and I(W2)=false,
          otherwise true</td>
        </tr>

        <tr>
          <td width="39%">not W</td>

          <td width="61%">true if I(W)=false, otherwise false</td>
        </tr>
      </tbody>
    </table>
    <br />
     <br />


    <p>If B is a mapping from a set W of variables into ID, then define
    [I+B] to be the interpretation which is like I except that
    [I+B](?v)=B(?v) for any variable ?v in W.</p>

    <table width="90%" border="1" summary="rules">
      <tbody>
        <tr>
          <td width="39%"><strong>if E is:</strong></td>

          <td width="61%"><strong>then I(E) is:</strong></td>
        </tr>

        <tr>
          <td width="39%">(forall (?v1,...,?vn) W)</td>

          <td width="61%" class="new">false if [I+B](W)=false for some
          mapping B from {?v1,...,?vn} into ID, otherwise true</td>
        </tr>

        <tr>
          <td width="39%">(exist (?v1,...,?vn) W)</td>

          <td width="61%" class="new">true if [I+B](W)=true for some
          mapping B from {?v1,...,?vn} into ID, otherwise false</td>
        </tr>
      </tbody>
    </table>
    <br />
     <br />
    Finally, a knowledge base is considered to be true if and only if
    all its elements are true, .i.e. to be a conjunction of its
    elements.

    <p>Intuitively, the meaning of an expression containing free
    variables is not well specified (it is formally specified, but the
    interpretation of the free variables is arbitrary.) To resolve any
    confusion, we impose a familiar convention by which any free
    variables in a sentence of a knowledge base are considered to be
    universally quantified at the top level of the expression in which
    they occur. (Equivalently, one could insist that all variables in
    any knowledge-base expression be bound by a quantifier in that
    expression; this would force the implicit quantification to be made
    explicit.)</p>

    <p>These definitions are quite conventional. The only unusual
    features are the incorporation of special-name values into the
    domain, the use of an explicit extension mapping, the fact that
    relations are not required to have a fixed arity, and the
    description of functions as a class of relations.</p>

    <p>The explicit extension mapping is a technical device to allow
    relations to be applied to other relations without going outside
    first-order expressivity. We note that while this allows the same
    name to be used in both an individual and a relation position, and
    in a sense gives relations (and hence functions) a 'first-class'
    status, it does not incorporate any comprehension principles or
    make any logical assumptions about what relations are in the
    domain. Notice that no special semantic conditions were invoked to
    treat variables in relation position differently from other
    variables. In particular, the language makes no comprehension
    assumptions whatever. The resulting language is first-order in all
    the usual senses: it is compact and satisfies <span class="new">the
    downward Skolem-Lowenheim property</span>, for example, and the
    usual machine-oriented inference processes still apply, in
    particular the unification algorithm. (One can obtain a translation
    into a more conventional syntax by re-writing every atomic sentence
    using a rule of the form R(t1,...,tn) =&gt; Holds(R, t1,...,tn),
    where 'Holds' is a 'dummy' relation indicating that the relation R
    is true of the remaining arguments. The presentation given here
    eliminates the need for this artificial translation, but its
    existence establishes the first-order properties of the language.
    <span class="new">To translate a conventional first-order syntax
    into the L<sub>base</sub> form, simply qualify all quantifiers to
    range only over non-<em>Relation</em>s.</span> The issue is further
    discussed in (Hayes &amp; Menzel ref). )</p>

    <p>Allowing relations with no fixed arity is a technical
    convenience which allows L<sub>base</sub> to accept more natural
    translations from some SWELs. It makes no significant difference to
    the metatheory of the formalism compared to a fixed-arity sytnax
    where each relation has a given arity. Treating functions as a
    particular kind of relation allows us to use a function symbol in a
    relation position (albeit with a fixed arity, which is one more
    than its arity as a function); this enables some of the
    translations to be specified more efficiently.</p>

    <p>As noted earlier, incorporating special name interpretations (in
    particular, integers) into the domain takes L<sub>base</sub>
    outside strict first-order compliance, but these domains have
    natural recursive definitions and are in common use throughout
    computer science. Mechanical inference systems typically have
    special-purpose reasoners which can effectively test for
    satisfiability in these domains. Notice that the incorporation of
    these special domains into an interpretation does not automatically
    incorporate all truths of a full theory of such structures into
    L<sub>base</sub>; for example, the presence of the integers in the
    semantic domain does not in itself require all truths of arithmetic
    to be valid or provable in L<sub>base</sub>.</p>

    <h3 id="axiom_schemas">2.4 Axiom schemes</h3>

    <p>An axiom scheme stands for an infinite set of L<sub>base</sub>
    sentences all having a similar 'form'. We will allow schemes which
    are like L<sub>base</sub> formulae except that expressions of the
    form "&lt;exp1&gt;<strong>...</strong>&lt;expn&gt;", ie two
    expressions of the same syntactic category separated by three dots,
    can be used, and such a schema is intended to stand for the
    infinite knowledge base containing all the L<sub>base</sub>
    formulae gotten by substituting some actual sequence of appropriate
    expressions (terms or variables or formulae) for the expression
    shown, which we call the <em>L<sub>base</sub> instances</em> of the
    scheme. (We have in fact been using this convention already, but
    informally; now we are making it formal.) For example, the
    following is an L<sub>base</sub> scheme:</p>

    <p>(forall
    (?v1<strong>...</strong>?vn)(R(?v1<strong>...</strong>?vn) implies
    Q(a, ?v2<strong>...</strong>?vn)))</p>

    <p>- where the expression after the first quantifier <span
    class="new">is an actual scheme expression, not a conventional
    abbreviation</span> - which has the following L<sub>base</sub>
    instances, among others:</p>

    <p>(forall (?x)(R(?x) implies Q(a, ?x)))</p>

    <p>(forall (?y,?yy,?z)(R(?y, ?yy, ?z) implies Q(a,?y,?yy,?z)))</p>

    <p>Axiom schemes do not take the language beyond first-order, since
    all the instances are first-order sentences and the language is
    compact, so if any L<sub>base</sub> sentence follows from (the
    infinite set of instances of) an axiom scheme, then it must in fact
    be entailed by some finite set of instances of that scheme.</p>

    <p>We note that L<sub>base</sub> schemes should be understood only
    as syntactic abbreviations for (infinite) sets of L<sub>base</sub>
    sentences when stating translation rules and specifying axiom sets.
    Since all L<sub>base</sub> expressions are required to be finite,
    one should not think of L<sub>base</sub> schemes as themselves
    being sentences; for example as making assertions, as being
    instances or subexpressions of L<sub>base</sub> sentences, or as
    being posed as theorems to be proved. Such usages would go beyond
    the first-order L<sub>base</sub> framework. (They amount to a
    convention for using infinitary logic: see [Hayes&amp; Menzel] for
    details.) This kind of restricted use of 'axiom schemes' is
    familiar in many textbook presentations of logic.</p>

    <h3><a id="entail" name="entail">2.5 Entailment</a></h3>

    <p><a id="defsatis" name="defsatis">Following conventional
    terminology, we say that I <i>satisfies</i> E if I(E)=true,</a> and
    that <a id="defentail" name="defentail">a set S of expressions
    <em>entails</em> E if every interpretation which satisfies every
    member of S also satisfies E.</a> If the set S contains schemes,
    they are understood to stand for the infinite sets of all their
    instances. Entailment is the key idea which connects
    model-theoretic semantics to real-world applications. As noted
    earlier, making an assertion amounts to claiming that the world is
    an interpretation which assigns the value true to the assertion. If
    A entails B, then any interpretation that makes A true also makes B
    true, so that an assertion of A already contains the same "meaning"
    as an assertion of B; we could say that the meaning of B is somehow
    contained in, or subsumed by, that of A. If A and B entail each
    other, then they both "mean" the same thing, in the sense that
    asserting either of them makes the same claim about the world. The
    interest of this observation arises most vividly when A and B are
    different expressions, since then the relation of entailment is
    exactly the appropriate semantic licence to justify an application
    inferring or generating one of them from the other. Through the
    notions of satisfaction, entailment and validity, formal semantics
    gives a rigorous definition to a notion of "meaning" that can be
    related directly to computable methods of determining whether or
    not meaning is preserved by some transformation on a representation
    of knowledge.</p>

    <p><a id="defvalid" name="defvalid">Any process or technique which
    constructs a well formed formula F<sub>output</sub> from some other
    F<sub>input</sub> is said to be <em>valid</em> if F<sub>input</sub>
    entails F<sub>output</sub>, otherwise <em>invalid.</em></a> Note
    that being an invalid process does not mean that the conclusion is
    false, and being valid does not guarantee truth. However, validity
    represents the best guarantee that any assertional language can
    offer: if given true inputs, it will never draw a false conclusion
    from them.</p>


<h2><a id="using" name="using">3.0 Using L<sub>base</sub> to define semantics
  of a SWEL</a></h2>
    Imagine we have a Semantic Web Language L<sub>i</sub>. To provide a
    semantics for L<sub>i</sub> using L<sub>base</sub>, we must
    provide:

    <ul>
      <li>
        <p>a procedure for translating expressions in L<sub>i</sub> to
        expressions in L<sub>base</sub>. This process will also
        consequently define the subset of L<sub>base</sub> that is used
        by L<sub>i</sub>.</p>
      </li>

      <li>
        <p>a set of vocabulary items introduced by L<sub>i</sub></p>
      </li>

      <li>

    <p>a set of axioms and/or axiom schemas (expressed in L<sub>base</sub> or
      L<sub>base</sub> schema) that capture the intended meanings of the terms
      in (2).</p>
      </li>
    </ul>
<p>Given a set of expressions G in L<sub>i</sub>, we apply the procedure above
  to obtain a set of equivalent well formed formulae in L<sub>base</sub>. We then
  conjoin these with the axioms associated with the vocabulary introduced by L<sub>i</sub>
  (and any other language upon which L<sub>i</sub> is layered). If there are associated
  axiom schemata, we appropriately instantiate these and conjoin them to these
  axioms. The resulting set, referred to as A(G), is an <i>axiomatic equivalent</i>
  of G.</p>
<p>There are several different 'styles' one could adopt for writing axiomatic
  equivalents. The most conservative amounts to simply transliterating the basic
  vocabulary of the SWEL into L<sub>base</sub> syntactic form, then relying on
  the axioms to determine their meaning. In cases where the axioms amount to an
  'iff' definition of the vocabulary item, however, this could be shortened by
  translating the SWEL vocabulary into the defined form directly, resulting in
  a simpler translation. For example, in giving an axiomatic equivalent for OWL-DL,
  the meaning of <code>rdfs:subClassOf </code> can be captured adequately by translating
  it directly into the form of a logical implication:</p>
<p>aaa <code>rdfs:subClassOf</code> bbb =(translates into)=&gt; <code>(forall
  (?x) (</code>aaa<code>(?x) implies</code> bbb<code>(?x) ))</code></p>
<p>This direct translation removes '<code>rdfs:subClassOf</code>' from the the
  axiomatic equivalent altogether, however, so makes it impossible to express
  other RDFS truths about the <code>rdfs:subClassOf</code> property. This would
  be acceptable if we were concerned only with OWL-DL, which imposes a syntactic
  restriction which forbids such propositions; but it is not acceptable when we
  wish to relate different SWELs to one another, which is the primary goal here.
  We therefore focus on the 'conservative' style of translation where the burden
  of expressing the meaning of the SWEL vocabulary falls largely on the axioms.</p>
<p>As an illustrative example, we give in the following table a <strong>sketch</strong>
  of the axiomatic equivalent for RDF graphs using the RDF(S) and OWL vocabularies,
  in the form of a translation from N-triples. <strong>Note, this should not be
  referred to as an accurate or normative semantic description.</strong></p>
<table width="100%" border="1" summary="Lbase translation">
  <caption>&nbsp;
  </caption>
  <tr class="othertable">
    <td ><strong>RDF expression E</strong></td>
    <td ><strong>L<sub>base</sub> expression <em>TR</em>[E]</strong><br/></td>
  </tr>
  <tr class="othertable">
    <td>a plain literal "sss"</td>
    <td>'sss' , with any internal occurrences of ''' prefixed with '\'</td>
  </tr>
  <tr class="othertable">
    <td>a plain literal "sss"@ttt</td>
    <td>the term <code>pair(</code>'sss'<em></em>,'ttt'<code>)</code></td>
  </tr>
  <tr class="othertable">
    <td>a typed literal <span >&quot;sss&quot;^^ddd </span></td>
    <td>the term <code>LiteralValueOf(</code>'sss'<em></em>,<em>TR</em>[ddd]<code>)</code></td>
  </tr>
  <tr class="othertable">
    <td>an RDF container membership property name of the form <code>rdf:_</code><em>nnn</em></td>
    <td><code>rdf-member(</code><em>nnn</em><code>)</code></td>
  </tr>
  <tr class="othertable">
    <td>any other URI reference aaa</td>
    <td>aaa or &lt;aaa&gt;</td>
  </tr>
  <tr class="othertable">
    <td>a blank node</td>
    <td>a variable (one distinct variable per blank node)</td>
  </tr>
  <tr class="othertable">
    <td>a triple <br />
      aaa<code> rdf:type </code>bbb<code> .</code></td>
    <td> <em>TR</em>[bbb]<code>(</code><em>TR</em>[aaa]<code>) and rdfs:Class(</code><em>TR</em>[bbb]<code>)</code></td>
  </tr>
  <tr class="othertable">
    <td>any other triple <br />
      aaa bbb ccc <code>.</code></td>
    <td><em>TR</em>[bbb]<code>(</code><em>TR</em>[aaa] <em>TR</em>[ccc]<code>)
      and rdf:Property(</code><em>TR</em>[bbb]<code>)</code></td>
  </tr>
  <tr class="othertable">
    <td>an RDF graph</td>
    <td>The existential closure of the conjunction of the translations of all
      the triples in the graph.</td>
  </tr>
  <tr class="othertable">
    <td>a set of RDF graphs</td>
    <td>The conjunction of the translations of all the graphs.</td>
  </tr>
</table>
<table summary="rdf Lbase axioms" width="100%" border="1">
  <caption>
  <br />
  RDF axioms
  </caption>
  <tr>
    <td  class="othertable"> <p><code>rdf:type(?x ?y) implies ?y(?x)</code></p>
      <p><code>rdf:Property(rdf:type)<br />
        rdf:Property(rdf:subject)<br />
        rdf:Property(rdf:predicate)<br />
        rdf:Property(rdf:object)<br />
        rdf:Property(rdf:first)<br />
        rdf:Property(rdf:rest)<br />
        rdf:Property(rdf:value)<br />
        rdf:List(rdf:nil)</code></p>
      <p><code><em>NatNumber</em>(?x) implies rdf:Property(rdf-member(?x))</code></p>
      <p><code>pair(?x ?y)=pair(?u ?v) iff (?x=?u and ?y=?v)</code> <em> ;; uniqueness
        for pairs, required by graph syntax rules. </em></p></td>
  </tr>
</table>
<table summary="rdfs axioms" width="102%" border="1">
  <caption>
  <br />
  RDFS axioms
  </caption>
  <tr>
    <td class="othertable"> <code>rdfs:Resource(?x)</code> <p><code>rdfs:Class(?y)
        implies (?y(?x) iff rdf:type(?x ?y))</code></p>
      <p><code>rdfs:range(?x ?y) implies ( ?x(?u ?v)) implies ?y(?v) )</code></p>
      <p><code>rdfs:domain(?x ?y) implies ( ?x(?u ?v)) implies ?y(?u) ) </code></p>
      <p><span class="newstuff"><code>r</code></span><code>dfs:subClassOf(?x ?y)
        implies<br />
        &nbsp;&nbsp;(rdfs:Class(?x) and rdfs:Class(?y) and (forall (?u)(?x(?u)
        implies ?y(?u)))</code></p>
      <p><code>rdfs:Class(?x) implies ( rdfs:subClassOf(?x ?x) and rdfs:subClassOf(?x
        rdfs:Resource) )</code></p>
      <p><code>( rdfs:subClassOf(?x ?y) and rdfs:subClassOf(?y ?z) ) implies rdfs:subClassOf(?x
        ?z)</code></p>
      <p><code>rdfs:subPropertyOf(?x,?y) implies<br />
        &nbsp;&nbsp;(rdf:Property(?x) and rdf:Property(?y) and (forall (?u ?v)(?x(?u
        ?v) implies ?y(?u ?v)))</code></p>
      <p><code>rdf:Property(?x) implies rdfs:subPropertyOf(?x ?x)</code></p>
      <p><code>( rdfs:subPropertyOf(?x ?y) and rdfs:subPropertyOf(?y ?z) ) implies
        rdfs:subPropertyOf(?x ?z)</code></p>
      <p><code>rdfs:ContainerMembershipProperty(?x) implies rdfs:subPropertyOf(?x
        rdfs:member)</code></p>
      <p><code>rdf:XMLLiteral(?x) implies rdfs:Literal(?x)</code></p>
      <p><code><em>String</em>(?y) implies rdfs:Literal(?y)</code></p>
      <p><code>(<em>String</em>(?x) and LanguageTag(?y)) implies rdfs:Literal(pair(?x,?y))</code></p>
      <p><code>rdfs:Datatype(?x) implies (?x(?y) implies rdfs:Literal(?y) )</code></p>
      <p><code><em>NatNumber</em>(?x) implies <br />
        (rdfs:ContainerMembershipProperty(rdf-member(?x)) and <br />
        rdfs:domain(rdf-member(?x) rdfs:Resource) and <br />
        rdfs:range(rdf-member(?x) rdfs:Resource) )</code></p>
      <p><code>rdfs:Class(rdfs:Resource)<br />
        rdfs:Class(rdf:Property)<br />
        rdfs:Class(rdfs:Class)<br />
        rdfs:Class(rdfs:Datatype)<br />
        rdfs:Class(rdf:Seq)<br />
        rdfs:Class(rdf:Bag)<br />
        rdfs:Class(rdf:Alt)<br />
        rdfs:Class(rdfs:Container)<br />
        rdfs:Class(rdf:List)<br />
        rdfs:Class(rdfs:ContainerMembershipProperty)<br />
        rdfs:Class(rdf:Statement)<br />
        rdf:Property(rdfs:domain)<br />
        rdf:Property(rdfs:range)<br />
        rdf:Property(rdfs:subClassOf)<br />
        rdf:Property(rdfs:subPropertyOf)<br />
        rdf:Property(rdfs:comment)<br />
        </code><code>rdf:Property(rdfs:seeAlso)<br />
        rdf:Property(rdfs:isDefinedBy)<br />
        rdf:Property(rdfs:label)<br />
        </code><em>;; the rest of the axioms are direct transcriptions of the
        <a href="http://www.w3.org/TR/rdf-mt/#RDFS_axiomatic_triples">RDFS axiomatic triples</a>,
        using the RDF to L<sub>base</sub> transcription rules:</em></p>
      <p><code>rdfs:domain(rdf:type rdfs:Resource)<br />
        rdfs:domain(rdfs:domain rdf:Property)<br />
        rdfs:domain(rdfs:range rdf:Property) <br />
        rdfs:domain(rdfs:subPropertyOf,rdf:Property)<br />
        rdfs:domain(rdfs:subClassOf rdfs:Class)<br />
        rdfs:domain(rdf:subject rdf:Statement)<br />
        rdfs:domain(rdf:predicate rdf:Statement)<br />
        rdfs:domain(rdf:object rdf:Statement)<br />
        rdfs:domain(rdf:member rdfs:Resource)<br />
        rdfs:domain(rdf:first rdf:List)<br />
        rdfs:domain(rdf:rest rdf:List)<br />
        rdfs:domain(rdfs:seeAlso rdfs:Resource)<br />
        rdfs:domain(rdfs:isDefinedBy rdfs:Resource)<br />
        rdfs:domain(rdfs:comment rdfs:Resource)<br />
        rdfs:domain(rdfs:label rdfs:Resource)<br />
        rdfs:domain(rdfs:value rdfs:Resource) </code></p>
      <p><code>rdfs:range(rdf:type rdfs:Class)<br />
        rdfs:range(rdfs:domain rdfs:Class)<br />
        rdfs:range(rdfs:range rdfs:Class)<br />
        rdfs:range(rdfs:subPropertyOf rdf:Property)<br />
        rdfs:range(rdfs:subClassOf rdfs:Class)<br />
        rdfs:range(rdf:subject rdfs:Resource)<br />
        rdfs:range(rdf:predicate rdfs:Resource)<br />
        rdfs:range(rdf:object rdfs:Resource)<br />
        rdfs:range(rdf:member rdfs:Resource)<br />
        rdfs:range(rdf:first rdfs:Resource)<br />
        rdfs:range(rdf:rest rdf:List)<br />
        rdfs:range(rdfs:seeAlso rdfs:Resource)<br />
        rdfs:range(rdfs:isDefinedBy rdfs:Resource)<br />
        rdfs:range(rdfs:comment rdfs:Literal)<br />
        rdfs:range(rdfs:label rdfs:Literal)<br />
        rdfs:range(rdfs:value rdfs:Resource) </code></p>
      <p><code>rdfs:subClassOf(rdf:Alt rdfs:Container)<br />
        rdfs:subClassOf(rdf:Bag rdfs:Container)<br />
        rdfs:subClassOf(rdf:Seq rdfs:Container)<br />
        rdfs:subClassOf(rdfs:ContainerMembershipProperty rdf:Property)</code></p>
      <p><code>rdfs:subPropertyOf(rdfs:isDefinedBy rdfs:seeAlso)</code></p>
      <p><code>rdfs:Datatype(rdf:XMLLiteral)<br />
        rdfs:subClassOf(rdfs:Datatype rdfs:Class)<br />
        </code></p></td>
  </tr>
</table>
<table width="100%" border="1" summary="rdf XMLliteral Lbase axioms">
  <caption>
  <br />
  RDF Datatyped Literal axioms
  </caption>
  <tr class="othertable">
    <td> <code>rdfs:Literal(LiteralValueOf(?x ?y)) iff ?y(LiteralValueOf(?x ?y))<br/>
      rdfs:Datatype(?y) implies rdfs:Class(?y)<br />
      rdfs:Datatype(?y) implies (exists (?x) ?y(?x) )</code></td>
  </tr>
</table>
<p>In addition, for each datatype named ddd , one needs a <em>datatype theory</em>
  consisting of all axioms of the following form, or the equivalent:</p>
<table width="100%" border="1">
  <tr>
    <td><p><code>rdfs:Datatype(</code>ddd<code>)</code><br />
        <code>ddd(LiteralValueOf('aaa' </code>ddd<code>))</code> where <code>aaa</code>
        is a legal lexical form for the datatype<br />
        <code>not ddd(LiteralValueOf('aaa' </code>ddd<code>))</code> where <code>aaa</code>
        is any string which is not a legal lexical form for the datatype.</p>
      </td>
  </tr>
</table>
<p>If there is some notational framework in (or added to) L<sub>base</sub> which
  enables one to write terms denoting the members of the value space of the datatype,
  then the database theory can also contain all true axioms of the form</p>
<p><code>LiteralValueOf('aaa' </code>ddd<code>) = [L2V(</code>ddd<code>,aaa)]</code></p>
<p>where the square brackets indicate the presence of the appropriate term for
  that value. For example, using decimal numerals to denote the integers, this
  could be all equations of the form</p>
<p><code>LiteralValueOf('345' xsd:integer) = 345</code></p>
<p>Such axioms, or equivalents, would be needed in order to connect the translation
  to other theories which used the more conventional notations.</p>
<p>In some cases, a datatype theory can be summarized in a finite number of axioms.
  <span class="newstuff">For example, the datatype theory for <code>xsd:string</code>
  can be stated by a single axiom:</span></p>
<p><code class="newstuff">(<em>String</em>(?x) iff xsd:string(?x) ) and (<em>String</em>(?x)
  implies LiteralValueOf(?x xsd:string) = ?x )</code></p>
<p>&nbsp;</p>
<h3><a id="rel" name="rel"></a>3.1 Relation between the two kinds
    of semantics</h3>
    Given a SWEL L<sub>i</sub>, we can provide a semantics for it either by providing
it with a model or by mapping it into L<sub>base</sub> and utilizing the model
theory associated with L<sub>base</sub>. Given a set of expressions G in Li and
its axiomatic equivalent in L<sub>base</sub> A(G), any L<sub>base</sub> interpretation
of A(G) defines an Li interpetation for G. The natural Li interpretation from
its own model theory will in general be simpler than the L<sub>base</sub> interpretation:
for example, interpretations of RDF will not make use of the universal quantification,
negation or disjunction rules, and the underlying structures need have no functional
relations. In general, therefore, the most 'natural' semantics for L<sub>i</sub>
will be obtained by simply ignoring some aspects of the L<sub>base</sub> interpretation
of A(G). (In category-theoretic terms, it will be the result of applying an appropriate
forgetful functor to the L<sub>base</sub> structure.) Nevertheless, this extra
structure is harmless, since it does not affect entailment in L<sub>i</sub> considered
in isolation; and it may be useful, since it provides a natural way to define
consistency across several SWELs at the same time, and to define entailment from
KBs which express content in different, or even in mixed, SWELs simultaneously.
For these reasons we propose to adopt it as a convention that the appropriate
notion of satisfaction for any SWEL expression G is in fact defined relative to
an L<sub>base</sub> interpretation of A(G).<br />
     <br />
The following diagram illustrates the relation between L<sub>i</sub>, L<sub>base</sub>,
G and interpretations of G according to the different model theories.<br />
     <br />

    <div class="c1">
      <img src="SLSWdiagOne.jpg" alt="Relation between model theories"
      width="433" height="385" />
    </div>
<p>The important point to note about the above diagram is that if the L<sub>i</sub>
  to L<sub>base</sub> mapping and model theory for L<sub>i</sub> are done consistently,
  then the two 'routes' from G to a satisfying interpretation will be equivalent.
  This is because the L<sub>i</sub> axioms included in the L<sub>base</sub> equivalent
  of G should be sufficient to guarantee that any satisfying interpretation in
  the L<sub>base</sub> model theory of the L<sub>base</sub> equivalent of G will
  contain a substructure which is a satisfying interpretation of G according to
  the L<sub>i</sub> model theory, and vice versa. </p>

    <p>The utility of this framework for combining assertions in
    several different SWELs is illustrated by the following diagram,
    which is an 'overlay' of two copies of the previous diagram.<br />
    </p>

    <div class="c1">
      <p><img src="SLSWdiagTwo.jpg"
      alt="Interpreting SWELs in combination" width="535"
      height="367" /></p>
    </div>

    <p>Note that the G1+G2 equivalent in this case contains axioms for
    both languages, ensuring (if all is done properly) that any
    L<sub>base</sub> interpretation will contain appropriate
    substructures for both sentences.</p>

    <p>If the translations into L<sub>base</sub> are appropriately
    defined at a sufficient level of detail, then even tighter semantic
    integration could be achieved, where expressions which 'mix'
    vocabulary from several SWELs could be given a coherent
    interpretation which satisfies the semantic conditions of both
    languages. This will be possible only when the SWELS have a
    particularly close relationship, however. In the particular case
    where one SWEL (the one used by G2) is layered on top of another
    (the one used by G1), the interpretations of G2 will be a subset of
    those of G1</p>

    <h3><a id="inaq" name="inaq">4.0 Inadequacies of
    L<sub>base</sub></a></h3>
    The L<sub>base</sub> described above has several deficiencies as a
    base system for the Semantic Web. In particular,

    <ul>
      <li>It does not capture the social meaning of URIs. It merely
      treats them as opaque symbols. A future web logic should go
      further towards capturing this intention.</li>

      <li>At the moment, L<sub>base</sub> does not provide any
      facilities related to the representation of time and change.
      However, many existing techniques for temporal representation use
      languages similar to L<sub>base</sub> in expressive power, and we
      are optimistic that L<sub>base</sub> can provide a useful
      framework in which to experiment with temporal ontologies for Web
      use.<br />
      </li>

      <li>It might turn out that some aspects of what we want to
      represent on the the semantic web requires more than can be
      expressed using the L<sub>base</sub> described in this document.
      In particular, L<sub>base</sub> does not provide a mechanism for
      expressing propositional attitudes or true second order
      constructs.</li>
    </ul>
    A future version of L<sub>base</sub>, which includes the above
    L<sub>base</sub> as a proper subset, might have to include such
    facilities.

    <h3><a id="acks" name="acks">5.0 Acknowledgements</a></h3>
    We would like to thank members of the RDF Core working group, Tim Berners-Lee,
Richard Fikes, Sandro Hawke, Jim Hendler and Peter Patel-Schneider for comments
on various versions of this document.
<h3><a id="refs" name="refs">6.0 References</a></h3>

    <dl>
      <dt>[Enderton]</dt>

      <dd>A Mathematical Introduction to Logic, H.B.Enderton,
      2<sup>nd</sup> edition, 2001, Harcourt/Academic Press.</dd>

      <dt>[Fikes &amp; McGuinness]</dt>

      <dd>R. Fikes, D. L. McGuinness, <a
      href="http://www.ksl.Stanford.EDU/people/dlm/daml-semantics/abstract-axiomatic-semantics.html">
      An Axiomatic Semantics for RDF, RDF Schema, and DAML+OIL</a>, KSL
      Technical Report KSL-01-01, 2001</dd>

      <dt>[Hayes &amp; Menzel]</dt>

      <dd>P. Hayes, C. Menzel, <a
      href="http://reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI2001.pdf">
      A Semantics for the Knowledge Interchange Format</a> , 6 August
      2001 (Proceedings of 2001 <a
      href="http://reliant.teknowledge.com/IJCAI01/">Workshop on the
      IEEE Standard Upper Ontology</a>)</dd>

      <dt><a id="ref-owl" name="ref-owl"></a>[OWL]</dt>

      <dd><a href="http://www.w3.org/TR/2002/WD-owl-ref-20021112/">Web
      Ontology Language (OWL) Reference Version 1.0</a>, Mike Dean, Dan
      Connolly, Frank van Harmelen, James Hendler, Ian Horrocks,
      Deborah L. McGuinness, Peter F. Patel-Schneider, and Lynn Andrea
      Stein. W3C Working Draft 12 November 2002. <a
      href="http://www.w3.org/TR/2002/WD-owl-ref-20021112/">This
      version</a> is http://www.w3.org/TR/2002/WD-owl-ref-20021112/ .
      Latest version is available at <a
      href="http://www.w3.org/TR/owl-ref/">http://www.w3.org/TR/owl-ref/</a>.</dd>

      <dt>[Marchiori &amp; Saarela]</dt>

      <dd>M. Marchioi, J. Saarela, <a
      href="http://www.w3.org/TandS/QL/QL98/pp/metalog.html">Query +
      Metadata + Logic = Metalog,</a> 1998</dd>

      <dt><a id="ref-rdf-concepts"
      name="ref-rdf-concepts"></a>[RDF-CONCEPTS]</dt>

      <dd><i><a
      href="http://www.w3.org/TR/2003/WD-rdf-concepts-20031010/">Resource
      Description Framework (RDF): Concepts and Abstract
      Syntax</a></i>, Klyne G., Carroll J. (Editors), World Wide Web
      Consortium Working Draft, 10 October 2003 (work in progress). <a
      href="http://www.w3.org/TR/2003/WD-rdf-concepts-20031010/">This
      version</a> is
      http://www.w3.org/TR/2003/WD-rdf-concepts-20031010/. The <a
      href="http://www.w3.org/TR/rdf-concepts/">latest version</a> is
      http://www.w3.org/TR/rdf-concepts/</dd>

      <dt><a id="ref-rdf-syntax"
      name="ref-rdf-syntax"></a>[RDF-SYNTAX]</dt>

      <dd><i><a
      href="http://www.w3.org/TR/2003/WD-rdf-syntax-grammar-20031010/">RDF/XML
      Syntax Specification (Revised)</a></i>, Beckett D. (Editor),
      World Wide Web Consortium Working Draft, 10 October 2003 (work in
      progress). <a
      href="http://www.w3.org/TR/2003/WD-rdf-syntax-grammar-20031010/">This
      version</a> is
      http://www.w3.org/TR/2003/WD-rdf-syntax-grammar-20031010/. The <a
      href="http://www.w3.org/TR/rdf-syntax-grammar/">latest
      version</a> is http://www.w3.org/TR/rdf-syntax-grammar/</dd>

      <dt><a id="ref_rdfmt" name="ref_rdfmt"></a> <a
      id="ref-rdf-semantics"
      name="ref-rdf-semantics"></a>[RDF-SEMANTICS]</dt>

      <dd><cite><a
      href="http://www.w3.org/TR/2003/WD-rdf-mt-20031010/">RDF
      Semantics</a></cite>, Hayes P. (Editor), World Wide Web
      Consortium Working Draft, 10 October 2003 (work in progress). <a
      href="http://www.w3.org/TR/2003/WD-rdf-mt-20031010/">This
      version</a> is http://www.w3.org/TR/2003/WD-rdf-mt-20031010/. The
      <a href="http://www.w3.org/TR/rdf-mt/">latest version</a> is
      http://www.w3.org/TR/rdf-mt/</dd>

      <dt><a id="ref-rdf-tests"
      name="ref-rdf-tests"></a>[RDF-TESTS]</dt>


  <dd><cite><a
      href="http://www.w3.org/TR/2003/WD-rdf-testcases-20031010/">RDF Test Cases</a></cite>,
    Grant J., Beckett D. (Editors) World Wide Web Consortium Working Draft, 5
    September 2003 (work in progress). <a
      href="http://www.w3.org/TR/2003/WD-rdf-testcases-20031010/">This version</a>
    is http://www.w3.org/TR/2003/WD-rdf-testcases-20031010/. The <a
      href="http://www.w3.org/TR/rdf-testcases/">latest version</a> is http://www.w3.org/TR/rdf-testcases/.</dd>

      <dt><a id="rdfmscite" name="rdfmscite"></a> [RDFMS]</dt>

      <dd><a
      href="http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/"><cite>Resource
      Description Framework (RDF) Model and Syntax</cite></a>, W3C
      Recommendation, 22 February 1999<br />
       <small><tt><a
      href="http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/">http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/</a></tt></small><br />

      </dd>

      <dt><a id="ref-rdf-primer"
      name="ref-rdf-primer"></a>[RDF-PRIMER]</dt>


  <dd><cite><a
      href="http://www.w3.org/TR/2003/WD-rdf-primer-20031010/">RDF Primer</a></cite>,
    Manola F., Miller E. (Editors), World Wide Web Consortium Working Draft, 5
    September 2003 (work in progress). <a
      href="http://www.w3.org/TR/2003/WD-rdf-primer-20031010/">This version</a>
    is http://www.w3.org/TR/2003/WD-rdf-primer-20031010/. The <a href="http://www.w3.org/TR/rdf-primer/">latest
    version</a> is http://www.w3.org/TR/rdf-primer/</dd>

      <dt><a name="ref-rdf-schema" id="ref-rdf-schema"></a><a
      name="RDFSRef" id="RDFSRef">[RDF-VOCABULARY]</a></dt>


  <dd><em><a
      href="http://www.w3.org/TR/2003/WD-rdf-schema-20031010/">RDF Vocabulary
    Description Language 1.0: RDF Schema</a></em>, Brickley D., Guha R.V. (Editors),
    World Wide Web Consortium, November 2002. Consortium Working Draft, 10 October
    2003 (work in progress). <a
      href="http://www.w3.org/TR/2003/WD-rdf-schema-20031010/">This version</a>
    is http://www.w3.org/TR/2003/WD-rdf-schema-20031010/. The <a href="http://www.w3.org/TR/rdf-schema/">latest
    version</a> is http://www.w3.org/TR/rdf-schema/</dd>

      <dt><a name="URIRef" id="URIRef">[URI]</a></dt>

      <dd>T. Berners-Lee, Fielding and Masinter, <a
      href="http://www.isi.edu/in-notes/rfc2396.txt">RFC 2396 - Uniform
      Resource Identifiers (URI): Generic Syntax</a>, August 1998.</dd>

      <dt><a name="WebOntRef" id="WebOntRef">[WebOnt]</a></dt>

      <dd><a href="http://www.w3.org/2001/sw/WebOnt/">The Web Ontology
      Working Group</a></dd>

      <dt><a name="XMLRef" id="XMLRef">[XML]</a></dt>

      <dd>T. Bray, J. Paoli, C.M. Sperberg.McQueen, E. Maler. <a
      href="http://www.w3.org/TR/REC-xml">Extensible Markup Language
      (XML) 1.0 (Second Edition)</a>, W3C Recommendation 6 October
      2000</dd>
    </dl>
	<h3><a id="change" name="change">7. Change Log</a></h3>
<p><font size="2">Since the version of 23 January, the definition of quoted strings
  has been modified to simplify character escaping; the syntax allowing names
  to be enclosed in &lt; &gt; introduced; and the 'XMLThing' category of special
  names deleted; it was underspecifed and not necessary. Several minor editorial
  changes have been made throughout the document (heading numbers corrected, etc.)
  . The example translation of RDF/RDFS has been updated so as to conform to the
  description given in the RDF Semantics document, and the discussion of axiomatic
  equivalents expanded.</font></p>
<p><font size="2">Thanks to Peter Patel-Schneider for critical comments on the
  earlier version. </font></p>
  </body>
</html>