You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
1108 lines
44 KiB
1108 lines
44 KiB
<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 & 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><quote id=foo about="theBook">
|
|
<dc:author>Ora</dc:author>
|
|
</quote>
|
|
<rdf:description href="#foo">
|
|
<dc:author>Ralph</dc:author>
|
|
<http:from>swick@w3.org</http:from>
|
|
</rdf:description></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><quote id=foo about="theBook">
|
|
<rdf:description href="#foo">
|
|
<dc:author>Ralph</dc:author>
|
|
<http:from>swick@w3.org</http:from>
|
|
</rdf:description>
|
|
<dc:author>Ora</dc:author>
|
|
</quote></pre>
|
|
|
|
<p></p>
|
|
|
|
<p>If it becomes common, would be even simpler is we defined a shortcut
|
|
element <head> to mean "about my enclosing parent element":</p>
|
|
<pre><quote about="theBook">
|
|
<head>
|
|
<dc:author>Ralph</dc:author>
|
|
<http:from>swick@w3.org</http:from>
|
|
<follows-from>http://www.org/catalog</follows-from>
|
|
</head>
|
|
<dc:author>Ora</dc:author>
|
|
</quote></pre>
|
|
|
|
<p></p>
|
|
|
|
<p>In fact one could make <quote> basically identical to
|
|
<rdf:Description> 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><foo:bar>
|
|
<head>
|
|
<include rdf:value="part1.rdf" />
|
|
<include rdf:value="part1.rdf" />
|
|
<include rdf:value="part1.rdf" />
|
|
</head>
|
|
</foo:bar></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><foo:bar>
|
|
<assert href="part1.rdf" />
|
|
<assert href="part1.rdf" />
|
|
<assert href="part1.rdf" />
|
|
</foo:bar></pre>
|
|
|
|
<p>Alternatively you can make a statement of the truth of the document:</p>
|
|
<pre><rdf:description about="part1.rdf">
|
|
<truth>1</truth>
|
|
</rdf:description></pre>
|
|
|
|
<p>This is strightforward too - and begs the question of what happens if you
|
|
say "0" instead of "1"</p>
|
|
<pre></quote>
|
|
<rdf:description about="#foo">
|
|
<truth>0</truth>
|
|
</rdf:description></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 & S2</p>
|
|
|
|
<p>more or less defines "&", 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><bar id="foo" about="http://ww.w3.org/"></pre>
|
|
<pre> <w3c:member>http://www.ibm.com/</w3c:member>
|
|
<not>
|
|
<w3c:member>http://www.soap.com/</w3c:member>
|
|
</not></pre>
|
|
<pre></bar></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><quote id="foo" about="http://www.w3.org/"></pre>
|
|
<pre> <w3c:member>http://www.soap.com/</w3c:member></pre>
|
|
<pre></quote>
|
|
<rdf:description about="#foo">
|
|
<truth>0</truth>
|
|
</rdf:description></pre>
|
|
|
|
<p>There is an overlap of semantics with <include>.</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><not>
|
|
<not>
|
|
<w3c:member>http://www.ibm.com/</w3c:member>
|
|
</not>
|
|
<not>
|
|
<w3c:member>http://www.soap.com/</w3c:member>
|
|
</not>
|
|
</not></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><alternatives>
|
|
<or>
|
|
<w3c:member>http://www.ibm.com/</w3c:member>
|
|
</or>
|
|
<or>
|
|
<w3c:member>http://www.soap.com/</w3c:member>
|
|
</or>
|
|
</alternatives></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><not>
|
|
<w3c:member>http://www.ibm.com/</w3c:member>
|
|
<not>
|
|
<w3c:member>http://www.soap.com/</w3c:member>
|
|
</not>
|
|
</not></pre>
|
|
|
|
<p>This similarly can be made more palatable to the human reader by using
|
|
synonuyms for <em>not</em>:</p>
|
|
<pre><if>
|
|
<w3c:member>http://www.ibm.com/</w3c:member>
|
|
<then>
|
|
<w3c:member>http://www.soap.com/</w3c:member>
|
|
</then>
|
|
</if></pre>
|
|
|
|
<h3><a name="Example">Example of trust statemement</a></h3>
|
|
|
|
<p>Above we had an example in which we invoked using <include> 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><foo:bar>
|
|
<head>
|
|
<if>
|
|
<ds:hash rdf:about=part1.rdf">
|
|
md5:1287129371237..12738127398712</ds:hash>
|
|
<then>
|
|
<include rdf:value="part1.rdf" />
|
|
</then>
|
|
</if>
|
|
<if>
|
|
<ds:signed-by rdf:about=part2.rdf">
|
|
rsa:a/1024/123hg1238912whh3983yd2734dg
|
|
</ds:signed-by>
|
|
<then>
|
|
<include rdf:value="part2.rdf" />
|
|
</then>
|
|
</if>
|
|
</head>
|
|
</foo:bar></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><quote id="foo" about="http://www.w3.org/"></pre>
|
|
<pre> <w3c:member>http://www.soap.com/</w3c:member></pre>
|
|
<pre></quote>
|
|
<rdf:description about="#foo">
|
|
<true-for-all>http://www.soap.com/</true-for-all>
|
|
</rdf:description></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><forall id="baz" var="x" rdf:about="#x">
|
|
<if>
|
|
<w3c:memberOf>http://www.w3.org/</w3c:memberOf>
|
|
<then>
|
|
<w3c:canAccess>http://www.w3.org/Member</w3c:canAccess>
|
|
<exists var="rep">
|
|
<w3c:acMember>#rep</w3c:acMember>
|
|
<w3c:employee>#rep</w3c:acMember>
|
|
</exists>
|
|
</then>
|
|
</if>
|
|
</forall></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 &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> <rdf:Description aboutEach="#pages">
|
|
|
|
<s:Creator>Ora Lassila</s:Creator>
|
|
|
|
</rdf:Description> </pre>
|
|
|
|
<p>This we can now explain as meaning</p>
|
|
|
|
<p></p>
|
|
<pre><forall var="x">
|
|
<if>
|
|
<rdf:li for="#pages" value="#x">
|
|
<then>
|
|
<s:Creator for="#x">Ora Lassila</s:Creator>
|
|
</then>
|
|
</if>
|
|
</forall></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><forall var="x">
|
|
<if rdf:about="#list">
|
|
<w3c:member "id=statement"
|
|
about="http://www.w3.org/"><var ref="#x">
|
|
</w3c:member>
|
|
<then>
|
|
<implies rdf:value="#statement" />
|
|
</then>
|
|
</if>
|
|
</forall>
|
|
<foo:container id="list"
|
|
rdf:about="http://www.w3.org/">
|
|
<w3c:member>http://www.ibm.com/"</w3c:member>
|
|
<w3c:member>http://www.hp.com/"</w3c:member>
|
|
<w3c:member>http://www.netscape.com/"</w3c:member>
|
|
<w3c:member>http://www.sun.com/"</w3c:member>
|
|
<w3c:member>http://www.acme.com/"</w3c:member>
|
|
</foo:container></pre>
|
|
|
|
<p>Note that just as in normal algrebra one almaost always uses "For all"
|
|
with "such that", here one will almsot always use <forall> with
|
|
<if> and so the two could be combined to save space into, say,
|
|
<ifany></p>
|
|
<pre><ifany var="x" rdf:about="#list">
|
|
<w3c:member "id=statement"
|
|
about="http://www.w3.org/"><var ref="#x">
|
|
</w3c:member>
|
|
<then>
|
|
<implies rdf:value="#statement" />
|
|
</then>
|
|
</ifany>
|
|
<foo:container id="list"
|
|
rdf:about="http://www.w3.org/">
|
|
<w3c:member>http://www.ibm.com/"</w3c:member>
|
|
<w3c:member>http://www.hp.com/"</w3c:member>
|
|
<w3c:member>http://www.netscape.com/"</w3c:member>
|
|
<w3c:member>http://www.sun.com/"</w3c:member>
|
|
<w3c:member>http://www.acme.com/"</w3c:member>
|
|
</foo:container></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 <B about=x value=V> for some (x,V) then it will
|
|
also imply any statement <B about=y value=V> 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"><foo:container id="list"
|
|
rdf:about="http://www.w3.org/">
|
|
<w3c:member>http://www.ibm.com/"</w3c:member>
|
|
<w3c:member>http://www.hp.com/"</w3c:member>
|
|
<w3c:member>http://www.netscape.com/"</w3c:member>
|
|
<w3c:member>http://www.sun.com/"</w3c:member>
|
|
<w3c:member>http://www.acme.com/"</w3c:member>
|
|
</foo:container>
|
|
|
|
<object-definitive about="#list">:w3c:member
|
|
</object-definitive></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><forall id="baz" var="x" rdf:about="#x">
|
|
<if>
|
|
<w3c:memberOf>http://www.w3.org/</w3c:memberOf>
|
|
<then>
|
|
<w3c:canAccess>http://www.w3.org/Member</w3c:canAccess>
|
|
<exists var="rep">
|
|
<w3c:acMember>#rep</w3c:acMember>
|
|
<w3c:employee>#rep</w3c:acMember>
|
|
</exists>
|
|
</then>
|
|
</if>
|
|
</forall></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><forall var="x" v2="y" v3="z" rdf:about="#x">
|
|
<if>
|
|
<employee>
|
|
<name>#y</name>
|
|
<street>#s</name>
|
|
<zip>#z</zip>
|
|
<employee>
|
|
<then>
|
|
<em> [...]
|
|
</em> </then>
|
|
</if>
|
|
</forall></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><forall var="x" v2="y" v3="z" rdf:about="#x">
|
|
<if>
|
|
<rdf:type>http://www.w3.org/1999/a/empType</>
|
|
<z:name>#y</>
|
|
<z:street>#s</>
|
|
<z:zip>#z</>
|
|
<then>
|
|
<em> [...]
|
|
</em> </then>
|
|
</if>
|
|
</forall></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><rdfs:range about="#employer">http://www.w3.org/1999/a/empType</a></pre>
|
|
|
|
<p>(sp?) is a way of saying</p>
|
|
<pre><forall var="x" v2="y" rdf:about="#x">
|
|
<if>
|
|
<employer>#y</employer>
|
|
<then>
|
|
<rdf:type>http://www.w3.org/1999/a/empType</rdf:type>
|
|
<em></em> </then>
|
|
</if>
|
|
</forall></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><forall var="aPropertyName" v2="y" v3="aType" rdf:about="#x">
|
|
<if>
|
|
<rdfs:range about="#aPropertyName">#aType</a>
|
|
<then>
|
|
<if>
|
|
<#aPropertyName>#y</> <!-- oops! ->
|
|
<then>
|
|
<rdf:type about="#y">http://www.w3.org/1999/a/empType</rdf:type>
|
|
<em></em> </then>
|
|
</then>
|
|
</if>
|
|
</forall></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><#aPropertyName>#y</> <!-- oops! -></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><rdf:property pname="#aPropertyName">#y</> <!-- better! -></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><the pname="#mother" of="#a"></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)...) -> (exists(w).
|
|
prop(w,x)) & ((prop(x,y) & prop(z,y)) -> 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)..) -> (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 <follows-from> 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><a:record id="foo" about="http://ww.w3.org/"></pre>
|
|
<pre> <w3c:member>http://www.ibm.com/</w3c:member></pre>
|
|
<pre></a:record>
|
|
<rdf:description about="#foo">
|
|
<follows-from>http://www.w3.org/MemberList</follows-fromsource>
|
|
</rdf:description></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 & 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><ifany varid="x'>
|
|
@@@@@@
|
|
<then>
|
|
</then>
|
|
</ifany></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><implies rdf:about="#from" rdf:value="#responsible"></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><implies rdf:about="#part-of" rdf:value="#includes">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>
|