Toolbox.html 43.7 KB

Raw Blame History Permalink

<html>
<head>
  <title>The Semantic Toolbox -  on top of XML-RDF -  Ideas on Web
  Architecture</title>
  <style type="text/css">
.detail { font-size: 10pt}
.detail { }</style>
  <link rel="stylesheet" href="di.css">
  <!-- Changed by: tbl 19990524 -->
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
</head>

<body>
<p><a href="../"><img alt="W3" border="0" src="/Icons/WWW/w3c_home"
width="72" height="48"></a></p>

<p><em>Status: Personal ramblings, unfinished in many places. Abandon
requiements for consistency all ye who enter in.Created: 1999/06/18</em></p>

<p>This document was an attempt to build logical formulaue as closely as
possible on top of the RDF triple abstract syntax.  Another more recent
investigation in this direction is <a href="Notation3">Notation3</a><a></a>.
It investigates using XML for logic.</p>
<hr>

<p></p>

<p>In this document:</p>
<ul>
  <li><a href="#Assumed">Assumed Syntax</a></li>
  <li><a href="#Semantic1">Semantic Context</a></li>
  <li><a href="#Assertion">Assetion of another document
    (<code>include</code>, assert, truth)</a></li>
  <li><a href="#Logical">Logical expressions:  (not)</a>
    <p><a href="#Example">Example of trust statemement</a></p>
    <p><a href="#Quantifica">Quantification (for all, exists)</a></p>
  </li>
</ul>

<p></p>

<p></p>

<h1><a name="Semantic">The Semantic Toolbox: Building Semantics on top of
XML-RDF</a></h1>

<p></p>

<p>The XML syntax [] and the RDF model [] give the basics for semantics of
the Web, but it seems to me we need some conective tissue to work towark the
semantic web.  Basically, everything we think of as "data" on the Web forms a
set of logical statements. We need a unifying logical langauge for data - for
the machine interfaces to data systems -- in the same way that HTML was a
unifying language for human interfaces to information systems. This document
is an attempt at an existence proof to reassure one that the XML/RDF model
will be able to meet a number of requirements which have been proposed in the
community.  These include</p>
<ul>
  <li>Stating that a list is definitive;</li>
  <li>Making a reference contingent on a digital signature of the
  destination;</li>
  <li>Writing inference rules for linking old and new schemata;</li>
  <li>Expressing the equivalence of terms in different database schemas;</li>
  <li>...</li>
</ul>

<p>The need, of course, is to build a logic out of RDF, as naturally as
possible. We fail if the syntax becomes drmatically more cumbersome as we add
features; we win if we find that higher-oder statements look like natural XML
just as simple metadata assertions do. We fail if at every stage we have
introduced special XML syntax whose semantic is expressed in English; we win
if we find that we can build up the language by introducing new RDF
properties - especially those whose semantics can be expressed in RDF and the
preceding properties.</p>

<p>(Within this document, XML elements with namespace prefix are assumed to
be defined as pointing to something the reader can figure out, and unprefixed
element names are used for new features which are introduced in this
document. ).</p>

<h2><a name="Assumed">Assumed syntax</a></h2>

<p>I assume for the purposes of this paper a syntax for data in XML which is
now described in a <a href="Syntax.html">separate note on syntax</a>.</p>

<p></p>

<h2><a name="Semantic1">Semantic Context</a></h2>

<p>Assertions are not all equal. They are made in different documents by
different people with different guarantees. They may be refered to, and even
denied explicitly.  The context of an assertion is therefore indispensible to
its use.</p>

<p>Context is inherited though nested XML elements unless an element of the
following forms changes that.</p>

<p>When an assertion is verified, evidence as to its veracity is accumulated
and submitted to subjective criteria of trust assesment. While the eventual
trust criteria are subjective, the logic of what is meant when data is put on
the Web must be very well defined and unambiguous.</p>

<h3>On reification</h3>

<p>The RDF model currently is that of an (unordered) set of assertions. We
will demonstrate that this remains all that is needed to represent the new
langauge features. Every new feature can be introduced as a new RDF property.
However, we will see that this is an impractical way of actually processing
information, as it involves using RDF indirectly to describe the parts of a
statement instead of making it directly. This process (called reification) is
described in the RDF Model &amp; Syntax document. An RDF statement in a what
RDF called a model, but I call a <dfn>Formula</dfn>,  can be reified by four
triples. Three are needed to assert the subject, object, and predicates of
the assertion. One to assert that the triple is part of the given model (set
of triples) -- where  more than one model can exist. Reification therefore
blows up the storage requirement by a factor of four.  </p>

<p>There is also a problem when using a simple link between the context
formula and the statement, that it is necessary to specify definitively the
set of statements in a formula.  There are a number of ways of doing this,
incluing the DAML list "first/rest" method, giving the number of statements,
and giving the relationship as for example "item_2_of_5".  As these are
inter-convertible, the choice is not fundamental.</p>

<p>We will see how reification ends up being replied successively, making the
verbosity become quite unnacceptable as a practical technique for repreenting
formulae.  Therefore, while we will derive each language feature simply by
defining a new RDF property, to make it practically useful we will also need
a syntax which allows the new langauge to be written less verbosely</p>

<p>Reification turns what is an explict statement into a description of  a
statement which is not specifically asserted, but which is described and can
be talked about. In languages this is typically done by quotation. In RDF
synatax to date there is now way of doing this, so let as start with that as
then we can do anything.</p>

<h3 id="Quotation">Quotation</h3>

<p>There is no specific element for this yet, so let's assume an QUOTE which,
which allows one to talk about assertions without asserting them. In the
"Ralph said Ora wrote the book" example, "Ora wrote the book" is obviously
quoted.  We need a away of distinguising between things we said and we stand
by, and statements we wish to discuss.  This is going to be of primary
importance on the Web in which information from many sources is combined.  It
is a fundamental part of language design.  (The PICS label system uses it for
example.  In metadata, information about information, quotation is obviously
essential.).</p>

<p>One way would be</p>
<pre>&lt;quote id=foo about="theBook"&gt;
          &lt;dc:author&gt;Ora&lt;/dc:author&gt;
&lt;/quote&gt;
&lt;rdf:description href="#foo"&gt;
   &lt;dc:author&gt;Ralph&lt;/dc:author&gt;
   &lt;http:from&gt;swick@w3.org&lt;/http:from&gt;
&lt;/rdf:description&gt;</pre>

<p>Here the quoted part says that Ora wrote the book, and then the
description following it assert that Ralph made the assertion.  This not to
be confused with a quote which maintains that it itself was written by Ralph,
but for which the present author makes no claim of truth or anything else:</p>
<pre>&lt;quote id=foo about="theBook"&gt;
    &lt;rdf:description href="#foo"&gt;
       &lt;dc:author&gt;Ralph&lt;/dc:author&gt;
       &lt;http:from&gt;swick@w3.org&lt;/http:from&gt;
    &lt;/rdf:description&gt;
    &lt;dc:author&gt;Ora&lt;/dc:author&gt;
&lt;/quote&gt;</pre>

<p></p>

<p>If it becomes common, would be even simpler is we defined a shortcut
element &lt;head&gt; to mean "about my enclosing parent element":</p>
<pre>&lt;quote about="theBook"&gt;
    &lt;head&gt;
       &lt;dc:author&gt;Ralph&lt;/dc:author&gt;
       &lt;http:from&gt;swick@w3.org&lt;/http:from&gt;
       &lt;follows-from&gt;http://www.org/catalog&lt;/follows-from&gt;
    &lt;/head&gt;
    &lt;dc:author&gt;Ora&lt;/dc:author&gt;
&lt;/quote&gt;</pre>

<p></p>

<p>In fact one could make &lt;quote&gt; basically  identical to
&lt;rdf:Description&gt; except disavowing of the assertions contained. [This
was, I understand, considered by the RDF working group].</p>

<h2><a name="Assertion">Assertion of another document</a></h2>

<p>(see also <a
href="http://www.daml.org/2000/12/reference.html#imports-def">daml:imports</a>
of Oct 2000 and and <a href="/2000/07/document-maintenance/">Dan's GET/PUT
model</a>)</p>

<p>Just as it is important to be able to exclude assertions within a document
from the set asserted directly by the document, it is equally as important to
be able to include assertions which are in fact not in the docoument. This is
easy to do with another property. It is, after all, a single assertion
indiacting that B should be believed to the extent that you believe A.</p>

<p></p>
<pre>&lt;foo:bar&gt;
    &lt;head&gt;
      &lt;include rdf:value="part1.rdf" /&gt;
      &lt;include rdf:value="part1.rdf" /&gt;
      &lt;include rdf:value="part1.rdf" /&gt;
    &lt;/head&gt;
&lt;/foo:bar&gt;</pre>

<p>This document, of some type we need not worry about, from the semantic
point of view is deemed to include the information in part1.rdf, part2.rdf,
and part3.rdf.  We use HEAD here as a shortcut for setting the subject to be
the current document.</p>

<p><span class="detail">(This is NOT a textual inclusion - it only brings
across the semantics of the other document, parsed with no context from this
one. If the destination document inlcldues HTML for SMIL, the text and
graphics for human consumption are NOT  invoked in any way!)</span></p>

<p>There is no information provided as to how or why to trust those
documents. The statememnt is only about the meaning of this document.  It is
importrnat to separate in the language the meaning and the trust.</p>

<p>(Deciding on a name for this is really diffictl, to get people to follow
this very basic logical function.  "Vouch"is a a nice word, meaning "asserts
the truth of".  "Imply" is nice word as it contains the fact that it is a
relationship between one document and another: if you don't believe the first
you don't have to believe the second. "Assert" or "IsTrue" are other
possibilites.)</p>

<p>It is overcomplicated to represent this as a binary relationship between
the current document and the document vouched for. It realy is a unary
relationship true(f) expressed in the current document. That would need an
XML shortcut rather than an RDF property, though, which would score less on
cleanliness.  But  it is simpler:</p>
<pre>&lt;foo:bar&gt;
      &lt;assert href="part1.rdf" /&gt;
      &lt;assert href="part1.rdf" /&gt;
      &lt;assert href="part1.rdf" /&gt;
&lt;/foo:bar&gt;</pre>

<p>Alternatively you can make a statement of the truth of the document:</p>
<pre>&lt;rdf:description about="part1.rdf"&gt;
   &lt;truth&gt;1&lt;/truth&gt;
&lt;/rdf:description&gt;</pre>

<p>This is strightforward too - and begs the question of what happens if you
say "0" instead of "1"</p>
<pre>&lt;/quote&gt;
&lt;rdf:description about="#foo"&gt;
   &lt;truth&gt;0&lt;/truth&gt;
&lt;/rdf:description&gt;</pre>

<h2><a name="Logical">Logical expressions: NOT</a></h2>

<p>We don't have a form for logical expressions for the semantic web,
although of course logical expression in human readers documents are covered
by MathML. The practical need for logical expressions has been apparent in
the IETF's work on profiling in the "conneg" group, and in the W3C's internal
work on access control.</p>

<p class="detail">(No comment needs to be made about the huge number of
languages which allow logical expression. In the classification of languages,
normally logic is introduced before the ability to make statements about
statements -- or rather, it was until Goedel. Here, the "first order"
question is taken backwards, in that RDF statements already break the "first
order" assumptions before basic logic has been introduced. <em>Not</em>
extends the toolbox to propositional logic.).</p>

<p>Of course we already have the logical "<strong>AND</strong>" construction
by juxtaposition. Two statements one after the other are both to be trusted
to the same extend as the context.  It is difficult contemplate a logical
system in which two statements cannot be considered together, so</p>

<p>{ S1, S2 }  ==  S1 &amp; S2</p>

<p>more or less defines "&amp;", and juxtaposition already exists, we already
have it.</p>

<p></p>

<p>One of the simplest forms of expression is NOT(x), which maps onto XML
most naturally as a single XML element:</p>

<p></p>
<pre>&lt;bar id="foo" about="http://ww.w3.org/"&gt;</pre>
<pre>    &lt;w3c:member&gt;http://www.ibm.com/&lt;/w3c:member&gt;
    &lt;not&gt;
        &lt;w3c:member&gt;http://www.soap.com/&lt;/w3c:member&gt;
    &lt;/not&gt;</pre>
<pre>&lt;/bar&gt;</pre>

<p>The <em>not</em> is transparent when it comes to the subject, but clearly
not when to comes to the trust!  It is an explicit assertion that the
contained assertion is false.</p>

<h3><em>Not</em> by reification</h3>

<p>I am not proposing that the best machine in practice to process the
language we are building is based directly on RDF triplets - but it is
important to ground new features in basic RDF. As RDF has little power at its
basic level, anything new has to be introduced by reification  - by
describing it in RDF. Hence, to say "not(node, property, value)", you have to
say, for example, "there is something which is an RDF property and  has a
subject of A and whose B property has vale C and is false". So in RDF, not
can be introduced by a new property which associates a boolean truth value
with another node.  Actually manipulating the information in this way is of
course not very efficient.</p>
<pre>&lt;quote id="foo" about="http://www.w3.org/"&gt;</pre>
<pre>    &lt;w3c:member&gt;http://www.soap.com/&lt;/w3c:member&gt;</pre>
<pre>&lt;/quote&gt;
&lt;rdf:description about="#foo"&gt;
   &lt;truth&gt;0&lt;/truth&gt;
&lt;/rdf:description&gt;</pre>

<p>There is an overlap of semantics with &lt;include&gt;.</p>

<p>There are therefore two ways of representing an expression containg not.
The strict RDF way, in which the only data is a set of triples, involved the
reification above.The way using the enhancd model simply encodes each</p>

<p>Before <em>not</em>, every assertion in an RDF database could be handled
independently, and deletion of a facts did not create untruth. However, with
<em>not</em>, it can, because we need to know the full set of terms in a
negated <em>and</em> expression to be able to deduce anything.</p>

<p><em>Not</em> is very powerful.  Given <em>not</em> and <em>and</em>, as
logicians and gate designers know, you can construct  many things.
Immediately, given that the contents of a <em>not</em> element are
<em>and</em>ed, we have a "nand" function. <span class="detail">["Nand" is
the Sheffer stroke which was shown in 1913 to be the only operator needed to
construct for a complete propositional logic system,  and which lin the 1970s
was the basic building block unit of the 7400 series logic]</span>.</p>

<p>With nand, you can construct, for example, <em>or</em>:</p>

<p></p>
<pre>&lt;not&gt;
    &lt;not&gt;
        &lt;w3c:member&gt;http://www.ibm.com/&lt;/w3c:member&gt;
    &lt;/not&gt;
    &lt;not&gt;
        &lt;w3c:member&gt;http://www.soap.com/&lt;/w3c:member&gt;
    &lt;/not&gt;
&lt;/not&gt;</pre>

<p>is equivalent to "either IBM is a member of W3C or soap.com is a member of
W3C".  It is a little clumsy, but looks more natural if you use synonyms:</p>
<pre>&lt;alternatives&gt;
    &lt;or&gt;
        &lt;w3c:member&gt;http://www.ibm.com/&lt;/w3c:member&gt;
    &lt;/or&gt;
    &lt;or&gt;
        &lt;w3c:member&gt;http://www.soap.com/&lt;/w3c:member&gt;
    &lt;/or&gt;
&lt;/alternatives&gt;</pre>

<p>Implication can also be constructed using <em>not</em>.  "If  soap.com is
a member then IBM is a member" can be written as "it is not true that
soap.com is a member and IBM is not a member", or:</p>
<pre>&lt;not&gt;
    &lt;w3c:member&gt;http://www.ibm.com/&lt;/w3c:member&gt;
    &lt;not&gt;
        &lt;w3c:member&gt;http://www.soap.com/&lt;/w3c:member&gt;
    &lt;/not&gt;
&lt;/not&gt;</pre>

<p>This similarly can be made more palatable to the human reader by using
synonuyms for <em>not</em>:</p>
<pre>&lt;if&gt;
    &lt;w3c:member&gt;http://www.ibm.com/&lt;/w3c:member&gt;
    &lt;then&gt;
        &lt;w3c:member&gt;http://www.soap.com/&lt;/w3c:member&gt;
    &lt;/then&gt;
&lt;/if&gt;</pre>

<h3><a name="Example">Example of trust statemement</a></h3>

<p>Above we had an example in which we invoked using &lt;include&gt; the
meaning in another document.  In same cases one might want to constrian the
simple invokation to protect the reader. We can use a conditional, for
example, to require a partiuclar checksum or digital signature:</p>

<p></p>
<pre>&lt;foo:bar&gt;
  &lt;head&gt;
    &lt;if&gt;
      &lt;ds:hash rdf:about=part1.rdf"&gt;
         md5:1287129371237..12738127398712&lt;/ds:hash&gt;
      &lt;then&gt;
          &lt;include rdf:value="part1.rdf" /&gt;
      &lt;/then&gt;
    &lt;/if&gt;
    &lt;if&gt;
      &lt;ds:signed-by rdf:about=part2.rdf"&gt;
         rsa:a/1024/123hg1238912whh3983yd2734dg
      &lt;/ds:signed-by&gt;
      &lt;then&gt;
          &lt;include rdf:value="part2.rdf" /&gt;
      &lt;/then&gt;
    &lt;/if&gt;
  &lt;/head&gt;
&lt;/foo:bar&gt;</pre>

<p>Here the document asserts the contents of part1 only if it has a certain
hash, and asserts the content of part2 only if it has a digital signature
which verifies with a partuclar public key. (the ds namespace is assumed to
exist to define hash and signed-by and is not frther discussed here apart
from to pint out that the hash value is an existing URI md5 scheme and that
the RSA key is just regarded as a URI too).</p>

<p>What is nice about this section is that this functionality has been
achieved using existing features.  The two statements may be a little
verbose, though it isn't obvious how one can make them very much more
compact.</p>

<p></p>

<h2>
<math xmlns="http://www.w3.org/1998/Math/MathML">
  <mtable>
    <mtr>
      <mtd>
      </mtd>
    </mtr>
  </mtable>
  <mtext></mtext>
</math>
 <a name="Quantifica">Quantification</a></h2>

<p>Examples above are very specific, when in fact many rules are made about
generalities. How would we add quantification to XML, the "for all" or "there
exists some"?   Like anything else, you can introduce it into RDF by
reifiying it (to descibe the expression's structure and then assert something
about the structure). Formally, then, to build it by tedious reification, one
would</p>

<p></p>
<pre>&lt;quote id="foo" about="http://www.w3.org/"&gt;</pre>
<pre>    &lt;w3c:member&gt;http://www.soap.com/&lt;/w3c:member&gt;</pre>
<pre>&lt;/quote&gt;
&lt;rdf:description about="#foo"&gt;
   &lt;true-for-all&gt;http://www.soap.com/&lt;/true-for-all&gt;
&lt;/rdf:description&gt;</pre>
<pre></pre>

<p>In this example (compare with the <em>not</em> reification above) the
element expressing "W3C has a member soap" statement is given the identifier
#foo, and then the assertion is made that the statement represented is true
even when "http://www.soap.com/" is replaced with any other value. This may
not be an inutitive way of quantifying things, and the variable name may seem
bizare, but it shows that we can derive quantification from a single added
RDF property, "true-for-all" [<a href="#Thanks">note</a>].</p>

<p>Quantification syntax for logic in XML</p>

<p>It is not obvious how to add this to a practical XML-based toolbox. One
can either try to layer it on to of XML, or extend XML. Here is one example
of layering it on top of  XML.  We use an XML element for the forall clause,
defining a variable at the same time in the ID space of the XML document. Any
reference to that variable within the clause is to be taken torefer to the
variable.</p>
<pre>&lt;forall id="baz" var="x" rdf:about="#x"&gt;
  &lt;if&gt;
    &lt;w3c:memberOf&gt;http://www.w3.org/&lt;/w3c:memberOf&gt;
    &lt;then&gt;
        &lt;w3c:canAccess&gt;http://www.w3.org/Member&lt;/w3c:canAccess&gt;
        &lt;exists var="rep"&gt;
           &lt;w3c:acMember&gt;#rep&lt;/w3c:acMember&gt;
           &lt;w3c:employee&gt;#rep&lt;/w3c:acMember&gt;
        &lt;/exists&gt;
    &lt;/then&gt;
  &lt;/if&gt;
&lt;/forall&gt;</pre>

<p>which, translated, means: For any X, if X is a member of W3C,  then X has
access to the member page, and there is some rep which is an advisory
commitee representative for X and also is an employee of X.</p>

<p>It is messy compared with mathematical symbols, but not compared with
typical XML.</p>

<p>The var attribute defines a variable in ID space (a subset of URI space),
so must have type IDREF because to have type ID in XML has the secondary
meaning of being an identifier for the element.</p>

<p class="detail">(An alternative might be to use XML enities in a magic new
form of entity &amp;x; or to simply make a new syntax which declared $x to be
a variable even tough you get really fed up with the dollar signs; or if you
want in interesting one to make a namespace which is defined to consist of
varibles. This latter would maybe confuse engines which didn't understand
it.)</p>

<p>(Note that the XML namespaces don't use scoping, but a "forall" clause
necessarily introduces a variable which only has sitgnficance within the
scope of the clause, element in this syntax. However, it may be referred to
from outside when a substitution is defined.  You will want to say for
example "substituing "John Doe" for the variable  foo.rdf#name  in
foo.rdf#rule1 yeilds ..." so the fact that the variable is afirst class
object may possibly be useful. Beware of course that you may want in one
forumula to use the quantified expression more than once using different
subsitutions)</p>

<p>In the 1.0 syntax spec there is a special syntax for a particular form of
quantification</p>

<p></p>
<pre> &lt;rdf:Description aboutEach="#pages"&gt;

    &lt;s:Creator&gt;Ora Lassila&lt;/s:Creator&gt;

&lt;/rdf:Description&gt;  </pre>

<p>This we can now explain as meaning</p>

<p></p>
<pre>&lt;forall var="x"&gt;
 &lt;if&gt;
   &lt;rdf:li for="#pages" value="#x"&gt;
   &lt;then&gt;
       &lt;s:Creator for="#x"&gt;Ora Lassila&lt;/s:Creator&gt;
   &lt;/then&gt;
 &lt;/if&gt;
&lt;/forall&gt;</pre>

<h3>Definitive lists</h3>

<p>A very common thing we need to express is a definitive set of things.</p>

<p>(Examples of definitive lists:</p>
<ul>
  <li>A definitive list of requirements for a document to be valid -
    validatable schema.</li>
  <li>An access control list (ACL) for a resource.</li>
  <li>A bank statement</li>
  <li>and so on...)</li>
</ul>

<p>When W3C gives a list of W3C members, it can not only tell you that if
someone is on the list they are a member, but also that if they are not on
the list they are not. The exclusivity of a list is a statement about a
document or part of a document. Here is a statement about the definitive
nature of a list, followed by a list:</p>
<pre>&lt;forall var="x"&gt;
  &lt;if rdf:about="#list"&gt;
    &lt;w3c:member "id=statement"
       about="http://www.w3.org/"&gt;&lt;var ref="#x"&gt;
    &lt;/w3c:member&gt;
    &lt;then&gt;
      &lt;implies rdf:value="#statement" /&gt;
    &lt;/then&gt;
  &lt;/if&gt;
&lt;/forall&gt;
&lt;foo:container id="list"
   rdf:about="http://www.w3.org/"&gt;
   &lt;w3c:member&gt;http://www.ibm.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.hp.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.netscape.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.sun.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.acme.com/"&lt;/w3c:member&gt;
&lt;/foo:container&gt;</pre>

<p>Note that just as in normal algrebra one almaost always uses "For all"
with "such that", here one will almsot always use &lt;forall&gt; with
&lt;if&gt; and so the two could be combined to save space into, say,
&lt;ifany&gt;</p>
<pre>&lt;ifany var="x" rdf:about="#list"&gt;
    &lt;w3c:member "id=statement"
       about="http://www.w3.org/"&gt;&lt;var ref="#x"&gt;
    &lt;/w3c:member&gt;
    &lt;then&gt;
      &lt;implies rdf:value="#statement" /&gt;
    &lt;/then&gt;
&lt;/ifany&gt;
&lt;foo:container id="list"
   rdf:about="http://www.w3.org/"&gt;
   &lt;w3c:member&gt;http://www.ibm.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.hp.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.netscape.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.sun.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.acme.com/"&lt;/w3c:member&gt;
&lt;/foo:container&gt;</pre>

<p></p>

<p>This is done using features defined to date.</p>

<p class="detail">(It is a little verbose, but we could make a shorthand for
the expression "list A is object-definitive for B", meaning  "If list A
implies the statement &lt;B about=x value=V&gt;  for some (x,V) then it will
also imply any statement &lt;B about=y value=V&gt; which is true. In other
words, "ibm is a member of w3c" in a  object-definitive list means that the
list will include all members of w3c, wheras in a subject-definitive list it
implies that the list contains all things ibm is a member of</p>
<pre><span class="detail">&lt;foo:container id="list"
   rdf:about="http://www.w3.org/"&gt;
   &lt;w3c:member&gt;http://www.ibm.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.hp.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.netscape.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.sun.com/"&lt;/w3c:member&gt;
   &lt;w3c:member&gt;http://www.acme.com/"&lt;/w3c:member&gt;
&lt;/foo:container&gt;

&lt;object-definitive about="#list"&gt;:w3c:member
      &lt;/object-definitive&gt;</span></pre>

<p><span class="detail">)</span></p>

<p></p>

<p></p>
<hr>

<p></p>

<h3>Functions</h3>

<p></p>

<p>A function is the ability to encapsulate meaning with the extraction of
parameters to be specified later.  This could map onto RDF and XML in a
number of ways, just as practical languages have various forms of
function.</p>

<p>When looking at the expoesion of data, a function becomes a compact
expression of a common expression.  The shorthand expression can take many
forms (positional or names parameters) but a clear choice for RDF is an RDF
node, whose actual arguments [the things which at function invokation replace
the formal parameters] are provided by a set of properties of that node.</p>

<p>The equivalent of the function "body" is then a set of information which
can be deduced from the node. An interesting point of the semantic web
philosophy is that, while one might think of "the" meaning of a function, in
fact the inference rules which express that are those provided by the
functions creator, but any other document might add its own rules.  In other
words, the function body is not a very useful term, and any expression about
the function will do. The example above</p>
<pre>&lt;forall id="baz" var="x" rdf:about="#x"&gt;
  &lt;if&gt;
    &lt;w3c:memberOf&gt;http://www.w3.org/&lt;/w3c:memberOf&gt;
    &lt;then&gt;
        &lt;w3c:canAccess&gt;http://www.w3.org/Member&lt;/w3c:canAccess&gt;
        &lt;exists var="rep"&gt;
           &lt;w3c:acMember&gt;#rep&lt;/w3c:acMember&gt;
           &lt;w3c:employee&gt;#rep&lt;/w3c:acMember&gt;
        &lt;/exists&gt;
    &lt;/then&gt;
  &lt;/if&gt;
&lt;/forall&gt;</pre>

<p>in fact is an example.  It states some implications of the concept of
membership of W3C.  You could take this to be definitive, but that is really
part of the trust model rather than the language.  In other words, W3C might
say that if an organization is a member of W3C then it has an AC
representative who is an employee. Another may maintian that any organization
which is is a member of W3C conmtains at least one smart employee.</p>

<p>I would expect that, where particular RDF nodes are intended to express
particular things by their creators, that the schema would have at least a
pointer to those things.</p>

<p>In the above example, the inference was just from a property of
membership: a property is used as binary predicate, but in general n-ary form
with multiple parameters could look like:</p>
<pre>&lt;forall var="x" v2="y" v3="z" rdf:about="#x"&gt;
  &lt;if&gt;
    &lt;employee&gt;
       &lt;name&gt;#y&lt;/name&gt;
       &lt;street&gt;#s&lt;/name&gt;
       &lt;zip&gt;#z&lt;/zip&gt;
    &lt;employee&gt;
    &lt;then&gt;
       <em> [...]
</em>    &lt;/then&gt;
  &lt;/if&gt;
&lt;/forall&gt;</pre>

<p>The basic RDF utility allows us to write all kinds of forms, and it may be
useful to pick one to make a common form. In the example above, the rule
applied to any node which is the employee (of anything) and has a name and a
street.  The property name "employee" is used like a function name. We can
use types for this instead:</p>
<pre>&lt;forall var="x" v2="y" v3="z" rdf:about="#x"&gt;
  &lt;if&gt;
    &lt;rdf:type&gt;http://www.w3.org/1999/a/empType&lt;/&gt;
    &lt;z:name&gt;#y&lt;/&gt;
    &lt;z:street&gt;#s&lt;/&gt;
    &lt;z:zip&gt;#z&lt;/&gt;
    &lt;then&gt;
       <em> [...]
</em>    &lt;/then&gt;
  &lt;/if&gt;
&lt;/forall&gt;</pre>

<p>Here the rule applies to any node which has been explicitly given the type
empType and has the given parameters.</p>

<p></p>

<p>Of course, these two things are linked by the RDF schema type
properties.</p>

<p></p>
<pre>&lt;rdfs:range about="#employer"&gt;http://www.w3.org/1999/a/empType&lt;/a&gt;</pre>

<p>(sp?) is a way of saying</p>
<pre>&lt;forall var="x" v2="y" rdf:about="#x"&gt;
  &lt;if&gt;
    &lt;employer&gt;#y&lt;/employer&gt;
    &lt;then&gt;
       &lt;rdf:type&gt;http://www.w3.org/1999/a/empType&lt;/rdf:type&gt;
<em></em>    &lt;/then&gt;
  &lt;/if&gt;
&lt;/forall&gt;</pre>

<p></p>

<p>In fact, while we are talking about functions we can use what we have now
to define bits of RDF Schema specification: we can start by defining what
"range" of a property means:</p>
<pre>&lt;forall var="aPropertyName" v2="y" v3="aType" rdf:about="#x"&gt;
  &lt;if&gt;
     &lt;rdfs:range about="#aPropertyName"&gt;#aType&lt;/a&gt;
     &lt;then&gt;
       &lt;if&gt;
          &lt;#aPropertyName&gt;#y&lt;/&gt;     &lt;!-- oops!  -&gt;
       &lt;then&gt;
          &lt;rdf:type about="#y"&gt;http://www.w3.org/1999/a/empType&lt;/rdf:type&gt;
<em></em>       &lt;/then&gt;
     &lt;/then&gt;
  &lt;/if&gt;
&lt;/forall&gt;</pre>

<p>I knew we would need  a way of invoking an RDF assertion by its full ID.
This is the identifier problem introduced above.</p>
<pre>&lt;#aPropertyName&gt;#y&lt;/&gt;     &lt;!-- oops!  -&gt;</pre>

<p>is what we need, and we can't in XML but we can instread define in the
basic RDF syntax an XML element to do that</p>
<pre>&lt;rdf:property pname="#aPropertyName"&gt;#y&lt;/&gt;     &lt;!-- better!  -&gt;</pre>

<p>which is not as clean in the sense of a consistent language but is but
good XML.</p>

<p>@@@</p>

<h3>Skolem functions.</h3>

<p>There are times when you may know that every person has a mother and you
may know that a person's mother is unique and so it is convenient to save the
bother of writing "for any x such that x is a's mother" and simply refer to
a's mother.  (This is similar in concept to skolem functions used to remove
quantifiers from expressions in symbolic logic.)</p>

<p>Maybe time for an XML shortcut:</p>

<p>&lt;the pname="#mother" of="#a"&gt;</p>

<p>can be thought of as a query as well.  It is well defined when the
property is unique, but when a property is not unique then it is not obvious
what sort of implicit quantification should be implied, and what the scope of
it would be ... not obvious. Two choices appear to match the choice of
definite and indefinite article in natural languages:</p>
<ol>
  <li>Make the use of the phrase within any forumula imply an assertion that
    the mother is unique:  F(..., THE(prop,x)...) -&gt;  (exists(w).
    prop(w,x)) &amp; ((prop(x,y) &amp; prop(z,y)) -&gt; x=z). Here THE(prop)
    is in caps as it is a special kind of function: in skolemization.,
    the(prop) is a new function added to the language to make a new langauge.
    THE not a first order function as it takes a predicate as an argument.
    Nor is it a function at all in that one can only generate a skolem
    sunction from the xistence statement.</li>
  <li>Make the use equivalent to an existence assertion but no uniqueness
    assertion.  Here F(.., A(prop,x)..) -&gt; (exists(w. prop(w,x)).</li>
</ol>

<p>The latter is the way it is usd in Skolemization, and I think we should
stick to that. Note that are NOT functions. They are not part of the
language. They are shortcuts.</p>

<p></p>

<h2><a name="Proof">Proof</a></h2>

<p>This is not about constructing a proof, but about transmitting a proof to
be validated. To define the proof language, one must define the powers of the
proof checking machine. In other words, do you have  to spoon-feed it every
atomic step, or is there a certain jump which it can make? This decision does
not have to be fundamental, in that you can imagine different vocabularies
for expressing a proof to different engines which have different capability.
At one extreme is the simplest logical engine for which everything must be
reduced to a connonical form of binary operators.  At the other extreme is
the proof "A follows-indirectly-from B" which involves the proof checker in
extensive (but bounded, or we don't call it a proof) searches. In between
lies the sound engineering compromise.</p>

<p>This will not be rigorous derivation, but a .</p>
<ol>
  <li>Canonicalization: The proof engine can be assumed to deduce one
    statement from another where the URIs involved (etc?) have the same value
    when canonicalized (equivalent values).</li>
  <li>Extraction: If an RDF assertion is made in an AND list (a normal list
    of RDF statements), then the proof engine can deduce it. (Does it need to
    b told the index of the ietm within the list? Or ID of the element?)</li>
  <li>Substitution: If a substitution is specified, the proof engine can
    generate the document which results from that subsitution.
    substitute(expression, variable)</li>
  <li>Implication: Given a proof of all the items in an AND list except for
    one, and given the negation of the AND list, can deduce the negation of
    the remaining item.</li>
  <li>Dereference: Given the statement that A follows-from B, and given B,
    deduce A.</li>
  <li>... and so on.</li>
</ol>

<p>[@@ref]</p>

<p>Now we need an expression to lead the proof-checker through a proof.
Let's assume taht canonicalization isimplciit in that it just involves
resolving relative URIs, and that otherwise exact string commparison implies
equivalence. (In practice there are often different URIs which yield the same
result but that can be an equivalence statement we can explicitly make if
ever we need to)</p>

<p>In the case that a given document [fragment] allows the proof checker to
deduce the required result directly, then all one needs is a single RDF
assertion to point it at the source from which it follows. We therefore
introduce the &lt;follows-from&gt; assertion</p>

<h3><a name="Follows-fr">Follows-from</a></h3>

<h4>Semantics:</h4>

<p>All the information A was derived from information in B.</p>

<h4>Comment:</h4>

<p>This is a tool for the "oh, yeah?" button. It allows one to trace back to
the origin of an assertion or assertions.  In order to verify the assertions,
the A is abandoned as being only a hint, and B is parsed to extract the same
meaning, and then verified. No representation is made about the language in
which B is written or why B should be believed.</p>

<h4>Example:</h4>
<pre>&lt;a:record id="foo" about="http://ww.w3.org/"&gt;</pre>
<pre>    &lt;w3c:member&gt;http://www.ibm.com/&lt;/w3c:member&gt;</pre>
<pre>&lt;/a:record&gt;
&lt;rdf:description about="#foo"&gt;
    &lt;follows-from&gt;http://www.w3.org/MemberList&lt;/follows-fromsource&gt;
&lt;/rdf:description&gt;</pre>

<p>The assertion that IBM is a member of W3C is implied by the W3C membership
list.</p>

<p>(Does the document assert that you can <em>still</em> deduce the
statements from the document? Yes, formally - an assrtion is an assertion.
However, if you don't trust the current document, typically you treat it as
an invitation to check the URI given.  Later we must deal with expiry with
time and "I found yyy in xxx but don't trust me: you check" statements which
do not lend explicit credance.)</p>

<p></p>

<p></p>

<h3>Specific derivation syntax</h3>

<p>...... @@@@@@</p>

<h3>Digital Signature and Trust</h3>

<p>The above deals with logic, when in fact any deducion in the real world or
on the Web is in fact made according to rules of trust.  On the Web, trust is
enhanced by the power of public key cryptography, and in particular, digital
signature.  The W3C Signed XML activity defines ways of signing an XML
document so that it can be shown to have been signed by the private key
corresponding to a give public key.</p>

<p>The following is a model of trust which seems powerful and seems general.
The basic concept is that of a statement being "assured by" a set of keys.
This is a new word and if you can thing of a better one, let me know.  It
means that the statement either has been made in a document (or part of a
document) whose signature has been verified with the key, or it has been
logically derived from such statements.  When it is logically derived from a
combination of statements assured by different sets of keys, then it is
assured by the union of the sets.</p>

<p><span class="detail">(You can think about it in terms of </span><em
class="detail">belief</em><span class="detail"> if you like, that if you
</span><em class="detail">believe</em><span class="detail"> all the keys in
the set you will </span><em class="detail">believe</em><span class="detail">
the statement, but that is not a useful analogy, as the model does not
require agents to actually "</span><em class="detail">believe</em><span
class="detail">" anything).</span></p>

<p></p>

<p>While from the rules defining assurance you might expect a logical
processor to accumulate a larger and larger key set as information is drawn
in from more and more sources, in fact the key set can reduce too.  Suppose
you have found on the web statment A signed by key Ka, and statment B signed
with key Kb.  If a third statement, signed with key K, says, "If A is signed
with Ka it is true, and if B is signed by Kb it is true," then you can deduce
A and B assured by K.  I would expect a typical trust engine to have one key
which it trusts basially from installation. For a webserver, for example, the
webmaster holds the key.  The server will only act on something which is
assured by that  key.  The various configuration files then contain trust
rules which delegate responsability for particular aspects of operation.</p>

<p>Many trust engines (whether or not they think of themselves as trust
engines) use simpler rules which are specicializations of this general model.
One is the simple trust boundary: "Trust the following keys for anything,
anything else for nothing". This is typical of the configuration of a web
browser for trusting applets. It obviously works because it is only reposible
for a certain decisions, and in fact the user is also involved with every one
as well - before the downloaded code is executed.  (This binary model of
trust leads to that binary concept of "<em>belief</em>")</p>

<p>The most general rule I can think of is of the form "if a statement of the
form x follows from key set y then deduce f(x)."  This would, of course,
typically be signed with another key.</p>

<p class="detail">(If we assume a key is a URI then we can declare keysets as
URIs too, by just using unique identifiers. This means that the problem of
dealing with sets can be hidden from the logic if we need to simplyify it. We
just declare a key set, give it mid: URI, and declare which RSA (say) keys it
contains. I don't think the key set idea is very fundamental - we just seem
to need it for completeness, so that we can extract the assuring keys from
sperate statements: from "A assues S and B assureds T", deduce "set {A B}
assures S and T". Maybe we can get away without that extraction, using
nesting instead, `A assures `B assures S &amp; T' ')</p>

<p></p>

<p>@@ homework: express published trust models in this general trust
model.</p>

<p>Examples of trust rules</p>

<p>"If K assures that y is a member of w3c then they are"</p>

<p>Doing this without any extra</p>
<pre>&lt;ifany varid="x'&gt;
   @@@@@@
   &lt;then&gt;
   &lt;/then&gt;
&lt;/ifany&gt;</pre>

<h2>Conclusion</h2>

<p></p>

<p>XML is clearly a (terrible, great) way of representing formal logic and
trust.</p>

<p></p>

<p></p>

<p></p>

<p></p>
<hr>

<h2>Assertions about topology - appendix</h2>

<p>These are some random assertions about assertions, in particular the
ropilogy of th DLGs which they make and the inferences which can be directly
made. Within this list, the semenatics are expliand for when the assertion is
made about A and the property  is given as having value B.</p>

<h3>A Implies B</h3>

<p>Semantics: Any assertion using the property type A implies an assertion
with the same subject node and value but with property type B.</p>

<p>Comment:</p>

<p>Domain and Range: The subject and object must both identify RDF
assertions.</p>

<p>Example</p>
<pre>&lt;implies rdf:about="#from" rdf:value="#responsible"&gt;</pre>

<p>If A is "from" B then A is repsonsible for B in this vocabulary.</p>

<h3>A Inverse B</h3>

<p>Semantics:  Any assertion using the property type A implies an assertion
with property type B in the reverse direction - ie whose subject was the
value of A and whose value was the subject of A.</p>

<p>Comment:Domain and Range: The subject and object must both identify RDF
assertions.</p>

<p>Note some relations are self-inverse. "Inverse" is self-inverse.</p>

<p>&lt;implies rdf:about="#part-of" rdf:value="#includes"&gt;If A is
"part-of" B then A "includes" B in this vocabulary.</p>

<p></p>

<h3>Acyclic, etc</h3>

<p>...@@@</p>

<p></p>

<h2>Terms introduced - A summary</h2>

<table border="1">
  <caption>Toolbox terms</caption>
  <tbody>
    <tr>
      <th>Term</th>
      <th>Language role</th>
      <th>axiomatic status</th>
      <th>semantics</th>
    </tr>
    <tr>
      <td>rdf:about</td>
      <td>xml attribute</td>
      <td>syntactic sugar</td>
      <td>set defualt rdf subject for element contents</td>
    </tr>
    <tr>
      <td>rdf:for</td>
      <td>xml attribute</td>
      <td>syntactic sugar</td>
      <td>override rdf subject for this element</td>
    </tr>
    <tr>
      <td>head</td>
      <td>xml element</td>
      <td>syntactic sugar</td>
      <td>set default rdf subject to parent element's node</td>
    </tr>
    <tr>
      <td>not</td>
      <td>xml element</td>
      <td>fundamental addition</td>
      <td>implies (reifiation and) denial of contents</td>
    </tr>
    <tr>
      <td>truth</td>
      <td>rdf property</td>
      <td>strict alternative to <em>not</em></td>
      <td>asserts boolean truth/falsity of document part</td>
    </tr>
    <tr>
      <td>if</td>
      <td>xml element</td>
      <td>synonym sugar</td>
      <td>synonym of not to create conditional</td>
    </tr>
    <tr>
      <td>then</td>
      <td>xml element</td>
      <td>syntactic sugar</td>
      <td>synonym of not to create conditional</td>
    </tr>
    <tr>
      <td>forall</td>
      <td>xml element</td>
      <td>fundamental</td>
      <td>quantification</td>
    </tr>
    <tr>
      <td>exists</td>
      <td>xml element</td>
      <td>syntactic sugar</td>
      <td>there exists - derivable from not(forall(not ...))</td>
    </tr>
  </tbody>
</table>

<p></p>

<p>[Notes</p>

<p><a name="Thanks">Thanks to Dan Connolly for pointing this out</a>.</p>

<p></p>

<h2>References</h2>

<p>these always seem to diappear... theer are many small lists of these, all
different.</p>

<p>Ban logic@@</p>

<p><a href="http://www.cs.princeton.edu/faculty/appel/">Appel</a>'set al.
work at Princeton on <a
href="http://www.cs.princeton.edu/sip/projects/pca/">Proof-Carrying
Authentication</a>: Proof-Carrying Authentication. Andrew W. Appel and Edward
W. Felten, 6th ACM Conference on Computer and Communications Security,
November 1999.</p>

<p></p>
<hr>
<small>Last change $Id: blank.html,v 1.1 1999/05/24 14:24:19 timbl Exp
$</small>
<address>
  Tim BL
</address>
</body>
</html>