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.
1273 lines
50 KiB
1273 lines
50 KiB
<!-- saved from url=(0063)file:///home/jmv/Documents/www.w3.org/DesignIssues/N3Logic.html -->
|
|
<!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 Mac OS X (vers 31 October 2006 - Apple Inc. build 15.3.6), see www.w3.org" />
|
|
<meta http-equiv="Content-Type" content=
|
|
"text/html; charset=us-ascii" />
|
|
|
|
<title>Notation 3 Logic</title>
|
|
<link href=
|
|
"file:///home/jmv/Documents/www.w3.org/DesignIssues/di.css" rel=
|
|
"stylesheet" type="text/css" />
|
|
</head>
|
|
|
|
<body xml:lang="en" lang="en">
|
|
<address>
|
|
Tim Berners-Lee, August 2005<br />
|
|
<small>$Revision: 1.152 $ of $Date: 2011/09/27 22:31:21 $</small><br />
|
|
Status: An early draft of a semi-formal semantics of the N3
|
|
logical properties.
|
|
</address>
|
|
|
|
<p><a href=
|
|
"file:///home/jmv/Documents/www.w3.org/DesignIssues/">Up to
|
|
Design Issues</a></p>
|
|
|
|
<h3>An RDF language for the Semantic Web</h3>
|
|
<hr />
|
|
<img alt="n3" src="file:///home/RDF/icons/n3_small" align=
|
|
"right" />
|
|
|
|
<h1>Notation 3 Logic</h1>This article gives an operational
|
|
semantics for Notation3 (N3) and some RDF properties for
|
|
expressing logic. These properties, together with N3's
|
|
extensions of RDF to include variables and nested graphs, allow
|
|
N3 to be used to express rules in a web environment. <br />
|
|
<br />
|
|
This is an informal semantics in that should be understandable by
|
|
a human being but is not a machine readable formal
|
|
semantics. This document is aimed at a logician wanting to a
|
|
reference by which to compare N3 Logic with other languages, and
|
|
at the engineer coding an implementation of N3 Logic and who
|
|
wants to check the detailed semantics.<br />
|
|
<br />
|
|
|
|
<p>These properties are not part of the N3 language, but are
|
|
properties which allow N3 to be used to express rules, and rules
|
|
which talk about the provenance of information, contents of
|
|
documents on the web, and so on. Just as OWL is expressed
|
|
in RDF by defining properties, so rules, queries, differences,
|
|
and so on can be expressed in RDF with the N3 extension to
|
|
formulae.</p>
|
|
|
|
<p>The log: namespace has functions, which have built-in meaning
|
|
for CWM and other software.</p>
|
|
|
|
<p>See also:</p>
|
|
|
|
<ul>
|
|
<li><a href="file:///home/jmv/2000/10/swap/log.n3">The schema
|
|
for the log: namespace</a></li>
|
|
|
|
<li><a href=
|
|
"file:///home/jmv/Documents/www.w3.org/DesignIssues/Diff.html">A
|
|
vocabulary for expressing differences between RDF
|
|
graphs</a></li>
|
|
|
|
<li><a href=
|
|
"http://lists.w3.org/Archives/Public/www-rdf-logic/2001Sep/0004.html">
|
|
a formal design for RDF/N3 context/scopes</a><br />
|
|
Dan Connolly to www-rdf-logic, Thu, Sep 06 2001</li>
|
|
</ul>
|
|
|
|
<p>The prefix log: is used below as shorthand for the
|
|
namespace <<a href=
|
|
"http://www.w3.org/2000/10/swap/log#">http://www.w3.org/2000/10/swap/log#</a>>.
|
|
See the <a href=
|
|
"file:///home/jmv/Documents/www.w3.org/2000/10/swap/logic.n3">schema</a>
|
|
for a summary.</p><br />
|
|
|
|
<h2><a name="motivation" id="motivation"></a>
|
|
Motivation</h2><br />
|
|
The motivation of the logic was to be useful as a tool in in open
|
|
web environment. The Web contains many sources of
|
|
information, with different characteristics and relationships to
|
|
any given reader. Whereas a closed system may be built
|
|
based on a single knowledge base of believed facts, an open
|
|
web-based system exists in an unbounded sea of interconnected
|
|
information resources. This requires that an agent be aware of
|
|
the provenance of information, and responsible for its
|
|
disposition. The language for use in this environment
|
|
typically requires the ability to express what document or
|
|
message said what, so the ability to quote subgraphs and match
|
|
them against variable graphs is essential. This
|
|
quotation and reference, with its inevitable possibility of
|
|
direct or indirect self-reference, if added directly to first
|
|
order logic presents problems such as paradox traps. To avoid
|
|
this, N3 logic has deliberately been kept to limited expressive
|
|
power: it currently contains no general first order
|
|
negation. Negated forms of many of the built-in
|
|
functions are available, however.<br />
|
|
<br />
|
|
A goal is that information, such as but not limited to rules,
|
|
which requires greater expressive power than the RDF graph,
|
|
should be sharable in the same way as RDF can be
|
|
shared. This means that one person should be able to
|
|
express knowledge in N3 for a certain purpose, and later
|
|
independently someone else reuse that knowledge for a different
|
|
unforeseen purpose. As the context of the later use is
|
|
unknown, this prevents us from making implicit closed assumptions
|
|
about the total set of knowledge in the system as a whole.<br />
|
|
<br />
|
|
Further, we require that other users of N3 in the web can express
|
|
new knowledge without affecting systems we have already
|
|
built. This means that N3 must be fundamentally monotonic:
|
|
the addition of new information from elsewhere, while it might
|
|
cause an inconsistency by contradicting the old information
|
|
(which would have to be resolved before the combined system is
|
|
used), the new information cannot silently change the meaning of
|
|
the original knowledge.<br />
|
|
<br />
|
|
The non-monotonicity of many existing systems follows from a form
|
|
of negation as failure in which a sentence is deemed false if it
|
|
not held within (or, derivable from) the<span style=
|
|
"font-style: italic;">current knowledge
|
|
base</span>. It is this concept of current knowledge
|
|
base, which is a variable quantity, and the ability to
|
|
indirectly make reference to it which causes the
|
|
non-monotonicity. In N3Logic, while a current
|
|
knowledge base is a fine concept, there is no ability to make
|
|
reference to it implicitly in the negative. The
|
|
negation provided is the ability only for a specific given
|
|
document (or, essentially, some abstract formula) to objectively
|
|
determine whether or not it holds, or allows one to derive, a
|
|
given fact. This has been called <span style=
|
|
"font-style: italic;">Scoped Negation As Failure</span>
|
|
(SNAF).<br />
|
|
<br />
|
|
|
|
<h2><a name="syntax" id="syntax"></a> Formal syntax</h2><br />
|
|
The syntax of N3 is defined by the <a href=
|
|
"http://www.w3.org/2000/10/swap/grammar/n3-report.html">context-free
|
|
grammar</a> This is available in machine-readable form in
|
|
<a href=
|
|
"http://www.w3.org/2000/10/swap/grammar/n3.n3"> Notation3</a>
|
|
and <a href=
|
|
"http://www.w3.org/2000/10/swap/grammar/n3.rdf">RDF/XML.</a><br />
|
|
|
|
<br />
|
|
The top-level production for an N3 document is
|
|
<http://www.w3.org/2000/10/swap/grammar/n3#document>.<br />
|
|
<br />
|
|
In the semantics below we will consider these productions using
|
|
notation as follows.<br />
|
|
<br />
|
|
|
|
<table style="text-align: left; width: 100%;" border="1"
|
|
cellpadding="2" cellspacing="2">
|
|
<tbody>
|
|
<tr>
|
|
<th>Production</th>
|
|
|
|
<th>N3 syntax examples</th>
|
|
|
|
<th>notation below for instances</th>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>symbol</td>
|
|
|
|
<td><span style="font-family: monospace;"><foo#bar>
|
|
<http://example.com/></span></td>
|
|
|
|
<td>c d e f</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>variable</td>
|
|
|
|
<td>Any symbol quantified by @forAll or @forSome in the
|
|
same or an outer formula.</td>
|
|
|
|
<td><span style="font-style: italic;">x y z</span></td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>formula</td>
|
|
|
|
<td><span style="font-family: monospace;">{ ...
|
|
}</span> or an entire document</td>
|
|
|
|
<td>F G H K</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>set of universal variables of F</td>
|
|
|
|
<td><span style="font-family: monospace;">@forAll :x,
|
|
:y.</span></td>
|
|
|
|
<td>uvF</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>set of existential variables of F</td>
|
|
|
|
<td><span style="font-family: monospace;">@forSome :z,
|
|
:w.</span></td>
|
|
|
|
<td>evF</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>set of statements of F</td>
|
|
|
|
<td></td>
|
|
|
|
<td>stF</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>statement</td>
|
|
|
|
<td> <span style=
|
|
"font-family: monospace;"><#myCar>
|
|
<#color> "green".</span></td>
|
|
|
|
<td>F<span style="font-style: italic;">i</span> or
|
|
{s p o}</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>string</td>
|
|
|
|
<td><span style="font-family: monospace;">"hello
|
|
world"</span></td>
|
|
|
|
<td>s</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>integer</td>
|
|
|
|
<td><span style="font-family: monospace;">34</span></td>
|
|
|
|
<td>i</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>list</td>
|
|
|
|
<td>( 1 2 ?x <a> )</td>
|
|
|
|
<td>L M</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>Element i of list L</td>
|
|
|
|
<td></td>
|
|
|
|
<td>L<span style="font-style: italic;">i</span><br /></td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>length of list</td>
|
|
|
|
<td></td>
|
|
|
|
<td>|L|</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>expression</td>
|
|
|
|
<td>see grammar</td>
|
|
|
|
<td>n m</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>Set*</td>
|
|
|
|
<td>{$ 1, 2, <a> $}</td>
|
|
|
|
<td>S T<br /></td>
|
|
</tr>
|
|
</tbody>
|
|
</table><br />
|
|
*The set syntax and semantics are not part of the current
|
|
Notation3 language but are under consideraton.<br />
|
|
|
|
<h2><a name="semantics" id="semantics"></a> Semantics</h2><br />
|
|
<span style="font-style: italic;">Note. The Semantics
|
|
of a generic RDF statement are not defined here. The
|
|
extensibility of RDF is deliberately such that a document may
|
|
draw on predicates from many sources. The statement {n
|
|
c m} expresses that the relationship denoted by c holds between
|
|
the things denoted by n and m. The meaning of
|
|
the statement {n c m} in general is defined by any
|
|
specification for c. The Architecture of the WWW specifies
|
|
informally how the curious can discover information about
|
|
the relation. It discusses how the architecture and management of
|
|
the WWW is such that a given social entity has jurisdiction over
|
|
certain symbols (though for example domain name ownership). This
|
|
philosophy and architecture is not discussed further
|
|
here. Here though we do define the semantics of
|
|
certain specific predicates which allow the expression of the
|
|
language. In analyzing the language the reader is
|
|
invited to consider statements of unknown meaning ground
|
|
facts. N3Logic defines the semantics of certain
|
|
properties. Clearly a system which recognizes further logical
|
|
predicates, beyond those defined here, whose meaning introduces
|
|
greater logical expressiveness would change the properties of the
|
|
logic.</span><br />
|
|
<br />
|
|
|
|
<h3>Simplifications</h3>N3 has a number of types of shortcut
|
|
syntax and syntactic sugar. For simplicity, in this article
|
|
we consider a language simpler the full N3 syntax referenced
|
|
above though just as expressive, in that we ignore most syntactic
|
|
sugar. The following simplifications are made.<br />
|
|
<br />
|
|
We ignore syntactic sugar of comma and semicolon as shorthand
|
|
notations. That is, we consider a simpler language in
|
|
which any such syntax has been expanded out. Loosely:<br />
|
|
<br />
|
|
|
|
<table style="text-align: left; width: 100%;" border="1"
|
|
cellpadding="2" cellspacing="2">
|
|
<tbody>
|
|
<tr>
|
|
<th>A sentence of the form</th>
|
|
|
|
<th>becomes two sentences</th>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>subject <span style=
|
|
"font-style: italic;">stuff</span> ; <span style=
|
|
"font-style: italic;">morestuff</span> .</td>
|
|
|
|
<td>subject <span style="font-style: italic;">stuff</span>
|
|
. subject <span style=
|
|
"font-style: italic;">morestuff</span> .</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>subject predicate <span style=
|
|
"font-style: italic;">stuff</span> , object .</td>
|
|
|
|
<td>subject predicate <span style=
|
|
"font-style: italic;">stuff</span> subject
|
|
predicate object .</td>
|
|
</tr>
|
|
</tbody>
|
|
</table><br />
|
|
<br />
|
|
For those familiar with N3, the other simplifications in the
|
|
language considered here are as follows.<br />
|
|
|
|
<ul>
|
|
<li> prefixes have been expanded and all qualified names
|
|
replaced with symbols using full URIs between angle
|
|
brackets.</li>
|
|
|
|
<li>The path syntax which uses "!" and "^" is
|
|
assumed expanded into its equivalent blank node form;</li>
|
|
|
|
<li>The "is ... of " backwards construction has been replaced
|
|
by the equivalent forwards direction syntax.</li>
|
|
|
|
<li>The "=" syntax is not used as shorthand for owl:sameAs. In
|
|
fact, we use = here in the text for value equality.</li>
|
|
|
|
<li>@keywords is not used</li>
|
|
|
|
<li>The @a shorthand for rdf:type is replaced with
|
|
a direct use of the full URI symbol for rdf:type</li>
|
|
|
|
<li>all ?x forms are replaced with explicit universal
|
|
quantification in the enclosing parent of the current
|
|
formula.</li>
|
|
</ul><br />
|
|
Notation3 has explicitly quantified existential variables as well
|
|
as blank nodes. The description below does not mention
|
|
blank nodes, although they are very close in semantics to
|
|
existentially quantified variables. We consider for
|
|
now a simpler language in which blank nodes have been replaced by
|
|
explicitly named variables existentially quantified in
|
|
the same formula.<br />
|
|
<br />
|
|
We have only included strings and integers, rather than the whole
|
|
set of RDF types an user-defined types.<br />
|
|
<br />
|
|
These simplifications will not deter us from using N3 shorthand
|
|
in examples where it makes them more readable, so the reader is
|
|
assumed familiar with them.<br />
|
|
|
|
<h2>Defining N3 Entailment</h2>The RDF specification defines a
|
|
very weak form of entailment, known as RDF entailment or simple
|
|
entailment. He we define the equivalent very simple
|
|
N3-entailment. This does not provide us with useful powers of
|
|
inference: it is almost textual inclusion, but
|
|
just has conjunction elimination (statement removal) ,
|
|
universal elimination, existential introduction and variable
|
|
renaming. Most of this is quite traditional. The
|
|
only thing to distinguish N3 Logic from typical logics is
|
|
the Formula, which allows N3 sentences to make statements about
|
|
N3 sentences. The following details are included for
|
|
completeness and may be skipped.<br />
|
|
|
|
<h3>Substitution</h3><span style=
|
|
"font-style: italic;">Substitution is defined to recursively
|
|
apply inside compound terms, as is usual. Note only
|
|
that substitution does descend into compund terms, while
|
|
substitution of owl:sameAs, discussed later, does
|
|
not.</span><br />
|
|
<br />
|
|
We define a substitution operator
|
|
σ<sub><span style="font-style: italic;">x</span>/m</sub>
|
|
which replaces occurrences of the variable <span style=
|
|
"font-style: italic;">x</span>. with the expression m. For
|
|
compound terms, substitution of a compound term (list,
|
|
formula or set) is performed by performing substitution of
|
|
each component, recursively.<br />
|
|
<br />
|
|
Abbreviating the substitution
|
|
σ<sub><span style="font-style: italic;">x</span>/m</sub>
|
|
as σ , we define substitution operator as
|
|
usual:<br />
|
|
<br />
|
|
σ<span style="font-style: italic;">x</span> = m
|
|
(<span style="font-style: italic;">x</span> is
|
|
replaced by m)<br />
|
|
σ<span style="font-style: italic;">y</span> = <span style=
|
|
"font-style: italic;">y</span> (y not
|
|
equal to x)<br />
|
|
σa = a (symbols and literals are
|
|
unchanged)<br />
|
|
σi = i<br />
|
|
σs = s <br />
|
|
σ( a b ... c ) = ( σa σb ...
|
|
σc )
|
|
(substitution goes into compound
|
|
terms)<br />
|
|
σ{$ a, b, ... c $} = {$ σa,
|
|
σb, ... σc $}<br />
|
|
uv σF = σ uvF<br />
|
|
ev σF = σ evF<br />
|
|
st σF = σ stF<br />
|
|
<br />
|
|
In general a substitution operator is the sequential application
|
|
of single substitutions:<br />
|
|
<br />
|
|
σ = σ<sub><span style=
|
|
"font-style: italic;">x</span>1/m1</sub>σ<sub><span style=
|
|
"font-style: italic;">x</span>2/m2</sub>σ<sub><span style=
|
|
"font-style: italic;">x</span>2/m2</sub> ...
|
|
σ<sub><span style=
|
|
"font-style: italic;">x</span>n/mn</sub><br />
|
|
<br />
|
|
|
|
<h3>Value equality </h3><br />
|
|
<span style="font-style: italic;">Value equality between terms is
|
|
defined in an ordinary way, compatible with RDF.</span><br />
|
|
<br />
|
|
For concepts which exist in RDF, we use RDF equality. This
|
|
is RDF node equality. These atomic concepts have a simple
|
|
form of equality.<br />
|
|
<br />
|
|
For lists, equality is defined as a pairwise matching.<br />
|
|
<br />
|
|
For sets, equality is defined as a mapping between equal terms
|
|
existing in each direction.<br />
|
|
<br />
|
|
For formulae, equality F = G is defined as a
|
|
substitution σ existing mapping variables to
|
|
variables. (Note that as here RDF Blank Nodes are
|
|
considered as existential variables, the substitution will map
|
|
b-nodes to b-nodes.)<br />
|
|
<br />
|
|
The table below is a summary for completeness.<br />
|
|
<br />
|
|
|
|
<table style="text-align: left; width: 100%;" border="1"
|
|
cellpadding="2" cellspacing="2">
|
|
<tbody>
|
|
<tr>
|
|
<th>Production</th>
|
|
|
|
<th>Equality</th>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>symbol</td>
|
|
|
|
<td>uri is equal unicode string</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>variable</td>
|
|
|
|
<td>variable name is equal unicode string</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>formula</td>
|
|
|
|
<td> F = G iff |stF| = |stG| and there is some
|
|
substitution σ such
|
|
that (∀<span style=
|
|
"font-style: italic;">i</span> . ∃<span style=
|
|
"font-style: italic;">j</span> . σ<span style=
|
|
"font-style: italic;">Fi</span> = σG<span style=
|
|
"font-style: italic;">j. </span>)</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>statement</td>
|
|
|
|
<td> Subjects are equal, predicates are equal, and
|
|
objects are equal</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>string</td>
|
|
|
|
<td> equal unicode string</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>integer</td>
|
|
|
|
<td> equal integer</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>list L = M</td>
|
|
|
|
<td> |L| = |M|
|
|
& (∀<span style=
|
|
"font-style: italic;">i</span> . L<span style=
|
|
"font-style: italic;">i</span> = M<span style=
|
|
"font-style: italic;">i )</span></td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>set S = T </td>
|
|
|
|
<td>(∀<span style="font-style: italic;">i</span>
|
|
. ∃<span style="font-style: italic;">j</span>
|
|
. S<span style="font-style: italic;">i</span> =
|
|
T<span style="font-style: italic;">j. </span>)
|
|
& (∀<span style=
|
|
"font-style: italic;">i</span> . ∃<span style=
|
|
"font-style: italic;">j</span> . S<span style=
|
|
"font-style: italic;">i</span> = T<span style=
|
|
"font-style: italic;">j. </span>)</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td>formula F = G</td>
|
|
|
|
<td>∃σ<span style=
|
|
"font-style: italic;">. </span>σ F
|
|
= σ G</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td style="font-style: italic;">unicode string</td>
|
|
|
|
<td>Unicode strings should be in canonical form. They are
|
|
equal if the corresponding characters have numerically
|
|
equal code points.</td>
|
|
</tr>
|
|
</tbody>
|
|
</table><br />
|
|
|
|
<h3>Conjunction</h3><span style="font-style: italic;">N3, like
|
|
RDF, has an implied conjunction, with its normal properties,
|
|
between the statements of a formula. </span><br />
|
|
<br />
|
|
The semantics of a formula which has no quantifiers (@forAll or
|
|
@forSome) are the conjunction of the semantics of the statements
|
|
of which it is composed.<br />
|
|
<br />
|
|
We define the conjunction elimination operator ce(i) of removing
|
|
the statement F<span style="font-style: italic;">i</span> from
|
|
formula F. By the conventional semantics of conjunction,
|
|
the ce(i) operator is truth-preserving. If you take a
|
|
formula and remove a statement from it it is still true.<br />
|
|
<br />
|
|
CE: From F follows ce(i)
|
|
F<br />
|
|
|
|
<h3>Existential quantification</h3><span style=
|
|
"font-style: italic;">Existential quantifiers and Universal
|
|
quantifiers have the usual qualities</span><br />
|
|
Any formula, including the <span style="font-style: italic;">root
|
|
formula</span> which matches the "document" production of the
|
|
grammar, may have a set of existential variables indicated
|
|
by an <span style="font-family: monospace;">@forSome</span>
|
|
declaration. This indicates that, where the formula
|
|
is considered true, it is true for at least one substitution
|
|
mapping the existential variables onto non-variables.<br />
|
|
<br />
|
|
As usual, we define a truth-preserving Existential
|
|
Introduction operator on formulae, that of introducing an
|
|
existentially quantified variable in place of any term. The
|
|
operation ei(x, n) is defined as<br />
|
|
|
|
<ol>
|
|
<li>Creation of a new variable <span style=
|
|
"font-style: italic;">x</span> which occurs nowhere
|
|
else</li>
|
|
|
|
<li>The application of σ<sub><span style=
|
|
"font-style: italic;">x</span>/n</sub> to F</li>
|
|
|
|
<li>The addition of<span style="font-style: italic;">x</span>
|
|
to evF.</li>
|
|
</ol><br />
|
|
EI: From F follows ei(x,n)
|
|
F for any <span style=
|
|
"font-style: italic;">x</span> not occurring anywhere else<br />
|
|
<br />
|
|
|
|
<h3>Universal quantification</h3><br />
|
|
Any formula, (including the root formula), may have a set
|
|
of universal variables. These are indicated by
|
|
<span style="font-family: monospace;">@forAll</span>
|
|
declarations. The scope of the @forAll is outside the
|
|
scope of any @forSome.<br />
|
|
<br />
|
|
|
|
<p>If both universal and existential quantification are specified
|
|
for the same context, then the scope of the universal
|
|
quantification is outside the scope of the existentials:</p>
|
|
<pre>
|
|
{ @forAll <#h>. @forSome <#g>. <#g> <#loves> <#h> }.
|
|
</pre>
|
|
|
|
<p>means</p>
|
|
|
|
<p>∀<#h> ( ∃<#g> ((
|
|
<span style="font-family: monospace;"> </span><#g>
|
|
<#loves> <#h> ))</p><br />
|
|
The semantics of @forAll is that for any substitution
|
|
σ = subst(<span style="font-style: italic;">x</span>, n)
|
|
where x member of uvF, if F is true then
|
|
σF is also true. Any @forAll declaration may also be
|
|
removed, preserving truth. Combining these, we define a
|
|
truth-preserving operation ue(x, n) such that
|
|
ue(x, n) F is formed by<br />
|
|
|
|
<ol>
|
|
<li>Removal of x from evF</li>
|
|
|
|
<li>Application of subst(x, n)</li>
|
|
</ol>We have the axiom of universal elimination<br />
|
|
<br />
|
|
UE: From F follows
|
|
ue(x, n) F for all x in evF<br />
|
|
As the actual variable used in a formula is quite irrelevant to
|
|
its semantics, the operation of replacing that variable with
|
|
another one not used elsewhere within the formula is
|
|
truth-preserving.<br />
|
|
<br />
|
|
|
|
<h3>Variable renaming</h3><br />
|
|
We define the operation of variable renaming
|
|
vr(<span style="font-style: italic;">x,y</span>) on F when x is a
|
|
member of uvF or is a member of evF.<br />
|
|
<br />
|
|
VR: From F follows
|
|
vr(<span style="font-style: italic;">x, y</span>) F
|
|
where <span style="font-style: italic;">x</span> is
|
|
in uvF or evF and <span style="font-style: italic;">y</span> does
|
|
not occur in F<br />
|
|
<br />
|
|
Occurrence in F is defined recursively in the same way as
|
|
substitution: <span style="font-style: italic;">x</span>
|
|
occurs in F iff σ<sub><span style=
|
|
"font-style: italic;">x</span>/n</sub>F is not equal to F for
|
|
arbitrary n.<br />
|
|
<br />
|
|
|
|
<h3>Union of formulae</h3>The union H = F∪G of two formulae F
|
|
and G is formed, as usual, as follows.<br />
|
|
<br />
|
|
A variable renaming operator is applied to G such that the
|
|
resulting formula G' has no variables which occur un-quantified
|
|
or differently quantified or existentially quantified in F, and
|
|
vice-versa. (F and G' may share universal
|
|
variables).ied or existentially quantified in F, and
|
|
vice-ver<br />
|
|
<br />
|
|
F∪G is then defined by:<br />
|
|
<br />
|
|
st(F∪G) = stF ∪ st G' ; ev(F∪G)
|
|
= evF ∪ evG' ; uv(F∪G) =
|
|
uvF ∪ uv G'<br />
|
|
<br />
|
|
<br />
|
|
|
|
<h3>N3 entailment</h3>
|
|
|
|
<p>The operators conjunction elimination, existential
|
|
elimination, universal introduction and variable
|
|
renaming are truth preserving. We define an
|
|
N3 entailment operator (τ) as any operator which is the
|
|
successive application of any sequence (possibly empty) of
|
|
such operators. We say a formula F n3-entails a
|
|
formula τ F. By a combination
|
|
of SE, EI, UE and VR, τ F logically
|
|
follows from F.</p><span style="font-style: italic;"> Note.
|
|
RDF Graph is a subclass of N3 formula. If F and G are
|
|
RDF graphs, only CI and EI apply and n3-entailment
|
|
reduces to simple entailment from RDF Semantics. (@@check
|
|
for any RDF weirdnesses)<br />
|
|
<br /></span>We have now defined this simple form of
|
|
N3-entailment, which amounts to little more than textual
|
|
inclusion in one expression of a subset of another. We
|
|
have not defined the normal collection of implication,
|
|
disjunction and negation which first order logic, as N3logic does
|
|
provide for first order negation. We have, in the
|
|
process, defined a substitution operation which we can now
|
|
use to define implication, which allows us to express
|
|
rules. <span style=
|
|
"font-style: italic;"><br /></span><br />
|
|
|
|
<h2>Logic properties and built-in functions</h2>We now define the
|
|
semantics of N3 statements whose predicate is one of a small set
|
|
of logic properties. These are statements whose truth can
|
|
be established by performing calculations, or by accessing the
|
|
web. <br />
|
|
<br />
|
|
One of our objectives was to make it possible to make statements
|
|
about, and to query, other statements such as the contents of
|
|
data in information resources on the web. We have, in
|
|
formulae, the ability to represent such sets of statements.
|
|
Now, to allow statements about them, we take some of the
|
|
relationships we have defined and give them URIs so that these
|
|
statements and queries can be written in N3.<br />
|
|
<br />
|
|
While the properties we introduced can be used simply as ground
|
|
facts in a database, is very useful to take advantage of
|
|
the fact that in fact they can be calculated. In some
|
|
cases, the truth or falsehood of a binary relation can be
|
|
calculated; in others, the relationship is a function so one
|
|
argument (subject or object of the statement) can be calculated
|
|
from the other.<br />
|
|
<br />
|
|
We now show how such properties are defined, and give examples of
|
|
how an inference system can use them. A motivation
|
|
here is to do for logical information what RDF did for data: to
|
|
provide a common data model and a common syntax, so that
|
|
extensions of the language are made simply by defining new
|
|
terms in an ontology. Declarative programing languages
|
|
like scheme[@@] of course do this. However, they differ in
|
|
their choice of pairs rather than the RDF binary relational model
|
|
for data, and lack the use of universal identifiers as
|
|
symbols. The goal with N3 was to make a
|
|
minimal extension to the RDF data model, so that the
|
|
same language could be used for logic and data, which in practice
|
|
are mixed as a colloidal solution in many real
|
|
applications.<br />
|
|
<br />
|
|
|
|
<h3>Calculated entailment</h3><br />
|
|
We introduce also a set of properties whose truth may be
|
|
evaluated directly by machine. We call these
|
|
"built-in" functions. The implementation as built-in
|
|
functions is not in general required for any
|
|
implementation of the N3 language, as they can always soundly be
|
|
treated as ground facts. However, their usefulness
|
|
derives from their implementation. We say that for example
|
|
{ 1 math:negation -1 } is entailed by
|
|
calculation. Like other RDF properties,
|
|
the set is designed to be extensible, as others can use URIs for
|
|
new functions. A much larger set of such properties is <a href=
|
|
"http://www.w3.org/2000/10/swap/doc/CwmBuiltins">described for
|
|
example in the CWM bultt-ins list</a>, and the semantics of those
|
|
are not described here.<br />
|
|
<br />
|
|
When the truth of a statement can be deduced because its
|
|
predicate is a built-in function, then we call the derivation
|
|
of the statement from no other evidence <span style=
|
|
"font-style: italic;">calculated entailment</span>.<br />
|
|
<br />
|
|
We now define a small set of such properties which provide the
|
|
power of N3 logic for inference on the web.
|
|
|
|
<h3>log:includes</h3>If a formula G n3-entails another
|
|
formula F, this is expressed in N3 logic as<br />
|
|
<br />
|
|
F <span style="font-family: monospace;">log:includes</span>
|
|
G.<br />
|
|
<br />
|
|
<span style="font-style: italic;">Note. In deference to the
|
|
fact that RDF treats lists not as terms but as things constructed
|
|
from first and rest pairs, we can view formulae which include
|
|
lists as including rdf:first and rdf:rest statements. The
|
|
effect on inclusion is that two other entailment operations are
|
|
added: the addition of any statement of the form
|
|
</span><span style=
|
|
"font-family: monospace; font-style: italic;">L rdf:first
|
|
n</span><span style="font-style: italic;">where n is the first
|
|
element of L, or L rdf:rest K where K is list forming the
|
|
remaining non-first elements of L. This is not essential
|
|
to a further understanding of the logic, nor to the operation of
|
|
a system which does not contain any explicit mention of the terms
|
|
rdf:first or rdf:rest.</span><br />
|
|
<br />
|
|
For the discussion of n3-entailment, clearly:<br />
|
|
<br />
|
|
From F and F log:includes G
|
|
logically follows G<br />
|
|
<br />
|
|
This can be calculated, because it is a mathematical operation on
|
|
two compound terms. It is typically used in a query to test
|
|
the contents of a formula. Below we will show how it can be
|
|
used in the antecedent of a rule.<br />
|
|
<br />
|
|
|
|
<h3>log:notIncludes</h3><br />
|
|
We write of formulae F and G: F log:notIncludes G if it is
|
|
<span style="font-weight: bold;">not</span> the case that G
|
|
n3-entails F.<br />
|
|
<br />
|
|
As a form of negation, log:notincludes is completely monotonic.
|
|
It can be evaluated by a mathematical calculation on the
|
|
value of the two terms: no other knowledge gained can influence
|
|
the result. This is the <span style=
|
|
"font-style: italic;">scoped negation as failure</span> mentioned
|
|
in the introduction. This is not a non-monotonic negation
|
|
as failure.<br />
|
|
<br />
|
|
|
|
<p><span style="font-style: italic;">Note on computation: To
|
|
ascertain whether G n3-entails F in the worst case involves
|
|
checking for all possible n3-entailment transformations
|
|
which are combinations of the variables which occur in G. This
|
|
operation may be tedious: it is strictly graph isomorphism
|
|
complete. However the use of symbols rather than variables
|
|
for a good proportion of nodes makes it much more tractable for
|
|
practical graphs. The ethos that it is a good idea to
|
|
give name things with URIs (symbols in N3) is a basic meme of web
|
|
architecture [AWWW]. It has direct practical
|
|
application in the calculation of n3-entailment, as comparison of
|
|
graphs whose nodes are labelled is much faster (of order n log
|
|
(n))) </span></p>
|
|
|
|
<h3><a name="log:implie" id="log:implie">log:implies</a></h3>The
|
|
log:implies property relates two formulae, expressing
|
|
implication. The shorthand notation for log:implies is
|
|
<span style="font-family: monospace;">=></span>
|
|
. A statement using log:implies, unlike log:includes,
|
|
cannot be calculated. It is not a built-in function,
|
|
but the predicate which allows the expression of a rule.<br />
|
|
<br />
|
|
<span style="font-style: italic;">The semantics of implication
|
|
are standard, but we elaborate them now for
|
|
completeness.</span><br style="font-style: italic;" />
|
|
<br />
|
|
F log:implies G is true if and only if when the formula F is true
|
|
then also G is true.<br />
|
|
<br />
|
|
MP: From F and
|
|
F => G follows G<br />
|
|
<br />
|
|
A statement in formula H is of the form F=>G can be
|
|
considered as rule, in which case, the subject F is the premise
|
|
(antecedent) of the rule, and the object G is the
|
|
consequent.<br />
|
|
<br />
|
|
Implication is normally used within a formula with universally
|
|
quantified variables.<span style=
|
|
"font-family: sans-serif;"><span style=
|
|
"font-style: italic;"><span style="font-weight: bold;"><br />
|
|
<br /></span></span></span>For example, universal quantifiers
|
|
are used with a rule in H as follows. Here H is
|
|
the formula containing the rules, and K the formula upon which
|
|
the rules are applied, which we can call the knowledge
|
|
base.<br />
|
|
<br />
|
|
If F => G is in H, and then for every σ which
|
|
is a transformation composed of universal eliminations of
|
|
variables universally quantified in H, then it also
|
|
follows that σF => σG. Therefore, for
|
|
every σ such that K includes σF,
|
|
σG follows from K.<br />
|
|
<br />
|
|
In the particular case that H and K are both the knowledge base,
|
|
or formula believed true at the top level, then<br />
|
|
<br />
|
|
GMP: From F => G
|
|
and σF follows σG
|
|
if σ is a transformation composed of
|
|
universal eliminations of variables universally quantified at the
|
|
top level.<br />
|
|
|
|
<h4>Filtering</h4>When a knowledge base (formula) contains a lot
|
|
of information, one way to filter off a subset is to run a set of
|
|
rules on the knowledge base, and take only the new data which is
|
|
generated by the rules. This is the filter
|
|
operation.<br />
|
|
<br />
|
|
When you apply rules to a knowledge base, the <span style=
|
|
"font-style: italic;">filter result</span> of rules in H applied
|
|
to K is the union of all σG for every statement F
|
|
=> G which is in H, for every σ which s
|
|
a transformation composed of universal eliminations of variables
|
|
universally quantified in H such that K includes σF.<br />
|
|
|
|
<h4>Repeated application of rules</h4>When rules are added back
|
|
repeatedly into the same knowledge base, in order to
|
|
prevent the unnecessary extra growth of the knowledge base,
|
|
before adding σG to it, there is a check to see
|
|
whether the H already includes σG, and if it does, the
|
|
adding of σG is skipped.<br style="font-style: italic;" />
|
|
<br />
|
|
Let the result of rules in H applied to K,
|
|
ρ<sub>H</sub>K, be the union of K with
|
|
all σG for every statement F => G which is in
|
|
H, for every σ which is a transformation
|
|
composed of universal eliminations of variables universally
|
|
quantified in H, such that K includes σF, and K does not
|
|
n3-entail σG.<br />
|
|
<br style="font-style: italic;" />
|
|
<br />
|
|
<span style="font-style: italic;">Note. This form of rule allows
|
|
existentials in the consequent: it is not datalog. It
|
|
is is clearly possible in a forward-chaining reasoner to generate
|
|
an unbounded set of conclusions with rules of the form
|
|
(using shorthand)</span><br style="font-style: italic;" />
|
|
<br style="font-style: italic;" />
|
|
<span style="font-style: italic;"> { ?x
|
|
a :Person } => { ?x :mother [ a :Person]
|
|
}.</span><br style="font-style: italic;" />
|
|
<br style="font-style: italic;" />
|
|
<span style="font-style: italic;">While this is a trap for the
|
|
unwary user of a forward-chaining reasoner, it was found to be
|
|
essential in general to be able to generate arbitrary RDF
|
|
containing blank nodes, for example when translating information
|
|
from one ontology into another.</span><br />
|
|
<br />
|
|
Consider the repeated application of rules in H to K,
|
|
ρ<sup style="font-style: italic;"><span style=
|
|
"font-style: italic;">i</span></sup><sub>H</sub>K. If there
|
|
are no existentially quantified variables in the consequents of
|
|
any of the rules in H, then this is like datalog, and there will
|
|
be some threshold <span style="font-style: italic;">n</span>
|
|
above which no more data is added, and there is a closure:
|
|
ρ<sup style="font-style: italic;"><span style=
|
|
"font-style: italic;">i</span></sup><sub>H</sub>K =
|
|
ρ<sup style="font-style: italic;"><span style=
|
|
"font-style: italic;">n</span></sup><sub>H</sub>K for all
|
|
<span style="font-style: italic;">i</span>><span style=
|
|
"font-style: italic;">n</span>. In fact in many practical
|
|
applications even with the datalog constraint removed, there is
|
|
also a closure. This ρ<sup>∞</sup><sub>H</sub>K
|
|
is the result of running a forward-chaining reasoner on H and
|
|
K.<br />
|
|
|
|
<h4>Rule Inference on the knowledge base</h4>In the case in which
|
|
rules are in the same formula as the data, the single rule
|
|
operation can be written ρ<sub>K</sub>K, and the
|
|
closure under rule application
|
|
ρ<sup>∞</sup><sub>K</sub>K<br />
|
|
<span style="font-weight: bold;"><br /></span> <span style=
|
|
"font-style: italic;">Cwm note: the --rules command line
|
|
option calculates ρ</span><sub style=
|
|
"font-style: italic;">K</sub><span style="font-style: italic;">K,
|
|
and the --think calculates ρ</span><sup style=
|
|
"font-style: italic;">∞</sup><sub style=
|
|
"font-style: italic;">K</sub><span style="font-style: italic;">K.
|
|
The --filter=H calculates the filter result of H on the
|
|
knowledge base.<br />
|
|
<br /></span>
|
|
|
|
<h3><span style="font-style: italic;">Examples</span></h3>Here a
|
|
simple rule uses log:implies.<br />
|
|
<br />
|
|
<pre>
|
|
@prefix log: <http://www.w3.org/2000/10/swap/log#>.<br />@keywords.<br />@forAll x, y, z. {x parent y. y sister z} log:implies {x aunt z}
|
|
</pre>
|
|
|
|
<p>This N3 formula has three universally quantified variables and
|
|
one statement. The subject of the statement, </p>
|
|
<pre>
|
|
{x parent y. y sister z}
|
|
</pre>
|
|
|
|
<p>is the antecedent of the rule and the object, </p>
|
|
<pre>
|
|
{x aunt z}
|
|
</pre>
|
|
|
|
<p>is the conclusion. Given data</p>
|
|
<pre>
|
|
Joe parent Alan.<br />Alan sister Susie.<br /><br />
|
|
</pre>
|
|
|
|
<p>a rule engine would conclude</p>
|
|
<pre>
|
|
Joe aunt Susie.
|
|
</pre>
|
|
|
|
<p>As a second example, we use a rule which looks inside a
|
|
formula:</p>
|
|
<pre>
|
|
@forAll x, y, z.<br />{ x wrote y.<br /> y log:includes {z weather w}.<br /> x livesIn z<br />} log:implies {<br /> Boston weather y<br />}.
|
|
</pre>
|
|
|
|
<p>Here the rule fires when x is bound to a symbol denoting some
|
|
person who is the author of a formula y, when the formula makes a
|
|
statement about the weather in (presumably some place) z, and x's
|
|
home is z. That is, we believe statements about the
|
|
weather at a place only from people who live there. Given
|
|
the data</p>
|
|
<pre>
|
|
Bob livesIn Boston.<br />Bob wrote { Boston weather sunny }.<br />Alice livesIn Adelaide.<br />Alice wrote { Boston weather cold }.
|
|
</pre>
|
|
|
|
<p>a valid inference would be</p>
|
|
<pre>
|
|
Boston weather sunny.
|
|
</pre>
|
|
|
|
<h3>log:supports</h3><br />
|
|
We say that F log:supports G if there is some sequence of
|
|
rule inference and/or calculated entailment and/or n3
|
|
entailment operators which when applied to F produce G.<br />
|
|
<br />
|
|
|
|
<h3>log:conclusion</h3><br />
|
|
<br />
|
|
The log:conclusion property expresses the relationship between a
|
|
formula and its deductive closure under operations of
|
|
n3-entailment, rule entailment and calculated entailment.
|
|
<br />
|
|
<br />
|
|
As noticed above, there are circumstances when this will not be
|
|
finite.<br />
|
|
<br />
|
|
log:conclusion is the transitive closure of log:supports.<br />
|
|
<br />
|
|
log:supports can be written in terms of log:conclusion and
|
|
log:includes.<br />
|
|
<br />
|
|
{ ?x log:supports ?y } if and only dan {
|
|
?x log:conclusion [ log:includes ?y ]}<br />
|
|
<br />
|
|
However, log:supports may be evaluated in many cases without
|
|
evaluating log:conclusion: one can determine whether y can be
|
|
derived from x in many ways, such as backward chaining, without
|
|
necessarily having to evaluate the (possibly infinite) deductive
|
|
closure.<br />
|
|
<br />
|
|
Now we have a system which has the capacity to do inference using
|
|
rules, and to operate on formulae. However, it
|
|
operates in a vacuum. In fact, our goal is that the
|
|
system should operate in the context of the web.<br />
|
|
<br />
|
|
|
|
<h2>Involving the Web</h2>We therefore expose the web as a
|
|
mapping between URIs and the information returned when such a URI
|
|
is dereferenced, using appropriate protocols. In
|
|
N3, the information resource is identified by a
|
|
symbol, which is in fact is its URI. In N3, information is
|
|
represented in formulae, so we represent the information
|
|
retrieved as a formula.<br />
|
|
Not all information on the web is, of course in N3. However the
|
|
architecture we design is that N3 should here be the interlingua.
|
|
Therefore, from the point of view of this system, the semantics
|
|
of a document is exactly what can be expressed in N3, no more and
|
|
no less.
|
|
|
|
<h3>log:semantics**</h3>
|
|
|
|
<p>c log:semantics F is true iff c is a document whose
|
|
logical semantics expressed in N3 is the formula F.</p>
|
|
|
|
<p>The relation between a document and the logical expression
|
|
which represents its meaning expressed as N3. The
|
|
Architecture of the World Wide Web [AWWW] defines algorithms by
|
|
which a machine can determine representations of
|
|
document given its symbol (URI). For
|
|
a representation in N3, this is the formula which corresponds to
|
|
the <span style="font-style: italic;">document</span> production
|
|
of the grammar. For a representation in
|
|
RDF/XML it is the formula which is the entire graph
|
|
parsed. For any other languages, it may be calculated
|
|
in as much a specification exists which defines the
|
|
equivalent N3 semantics for files in that language.</p>
|
|
|
|
<p>On the meaning of N3 formula</p>
|
|
|
|
<p>This is not of course the semantics of the document in
|
|
any absolute sense. It is the semantics expressed in
|
|
N3. In turn, the full semantics of an N3 formula are
|
|
grounded, in the definitions of the properties and classes
|
|
used by the formula. In the HTTP space in which
|
|
URIs are minted by an authority, definitive information about
|
|
those definitions may be found by dereferencing the URIs. This
|
|
information may be in natural language, in some
|
|
machine-processable logic, or a mixture. Two patterns
|
|
are important for the semantic web. </p>
|
|
|
|
<p>One is the grounding of properties and classes by defining
|
|
them in natural language. Natural language, of course,
|
|
is not capable of giving an absolute meaning to anything in
|
|
theory, but in practice a well written document, carefully
|
|
written by a group of people achieves a precision of definition
|
|
which is quite sufficient for the community to be able to
|
|
exchange data using the terms concerned. The other
|
|
pattern is the raft-like definition of terms in terms of related
|
|
neighboring ontologies.</p>
|
|
|
|
<p> @@@@ A full discussion of the grounding of meaning in a
|
|
web of such definitions is beyond the scope of this
|
|
article. Here we define only the operation semantics
|
|
of a system using N3.</p>
|
|
|
|
<p>@@@@ Edited up to here</p>The log:semantics of an N3
|
|
document is the formula achieved by parsing representation of the
|
|
document.<br />
|
|
(Cwm note: Cwm knows how to go get a document and parse N3 and
|
|
RDF/XML , in order to evaluate this. )<br />
|
|
<br />
|
|
Other languages for web documents may be defined whose N3
|
|
semantics are therefore also calculable, and so they could be
|
|
added in due course.<br />
|
|
See for example [GRDDL], [RDF/A], etc<br />
|
|
|
|
<p>However, for the purpose of the analysis of the language, it
|
|
is a convenient to consider the semantic web simply as a
|
|
binary 1:1 relation between a subset of symbols and
|
|
formulae.</p>
|
|
|
|
<p>For a document in Notation3, log:semantics is the<br />
|
|
log:parsedAsN3 of the log:contents of the document.<br />
|
|
<br /></p>
|
|
|
|
<h3>log:says</h3>log:says is defined by:<br />
|
|
<br />
|
|
F log:says G iff ∃ H .
|
|
<span style="font-family: monospace;">F log:semantics
|
|
H</span> and <span style=
|
|
"font-family: monospace;">H log:includes G</span>
|
|
<br />
|
|
<br />
|
|
In other words, loosely a document says something if a
|
|
representation of it in the sense of the Architecture of the
|
|
World Wide Web [AWWW] N3-entails it.<br />
|
|
<br />
|
|
The semantics of log:says are similar to that of says in
|
|
[PCA].<br />
|
|
<br />
|
|
|
|
<h2>Miscellaneous</h2>
|
|
|
|
<h3>log:Truth</h3>
|
|
|
|
<p>This is a class of true formulae. </p>
|
|
|
|
<p>From { F rdf:type log:Truth } follows
|
|
F </p>
|
|
|
|
<p>The cwm engine will process rules in the (indirectly
|
|
command-line specified) formula or any formula which that
|
|
declares to be a Truth. </p>
|
|
|
|
<p>The dereifier will output any described formulae which are
|
|
described as being in the class Truth. </p>This class is not
|
|
at all central to the logic.
|
|
|
|
<h2>Working with OWL</h2>
|
|
|
|
<p>@@ Summary</p>
|
|
|
|
<ul>
|
|
<li>owl:sameAs considered the same as N3 value equality for
|
|
data values. Axioms of
|
|
equality. log:equalTo and
|
|
log:notEqualTo compared with owl:SameAs. Compare
|
|
math and string equality, and SPARQL equality.</li>
|
|
|
|
<li>Operating in equality-aware mode.</li>
|
|
|
|
<li>No attempt at connecting OWL DL language with the N3
|
|
logic. </li>
|
|
|
|
<li>Use of functional properties of a datatype conflicting with
|
|
OWL DL.</li>
|
|
</ul>
|
|
|
|
<h2>Conclusion</h2>
|
|
|
|
<p>The semantics of N3 have been defined, as have some built-in
|
|
operator properties which add logical inference using rules to
|
|
the language, and allow rules to define inference which can be
|
|
drawn from specific web documents on the web, as a function of
|
|
other information about those documents.</p>
|
|
|
|
<p>The language has been found to have some useful practical
|
|
properties. The separation between the Notation3
|
|
extensions to RDF and the logic properties has allowed N3 by
|
|
itself to be used in many other applications directly, and to be
|
|
used with other properties to provide other functionality such as
|
|
the expression of patches (updates) [Diff].</p>
|
|
|
|
<p>The use of log:notIncludes to allow default reasoning without
|
|
non-monotonic behavior achieves a design goal for distributed
|
|
rule systems.</p><br />
|
|
<hr style="width: 100%; height: 2px;" />
|
|
**[Footnote: Philosophers may be distracted here into worrying
|
|
about the meaning of meaning. At least we didn't call this
|
|
function "meaning"! In as much as N3 is used as an interlingua
|
|
for interoperability for different systems, this for an N3 based
|
|
system is the meaning expressed by a document. One
|
|
reviewer was aghast at the definition of semantics as being that
|
|
of retrieval of a representation, its parsing and assimilation in
|
|
terms of the local common logical framework. I suspect however
|
|
that the meaning of the paper to the reviewer could be considered
|
|
quite equivalently the result of the process of
|
|
retrieval of a representation of the paper, its parsing by the
|
|
review, and its assimilation in terms of the reviewer's local
|
|
logical framework: a similar though perhaps imperfect
|
|
process.<br />
|
|
Of course, the semantics of many documents are not expressible in
|
|
logics at all, and many in logic but not in N3. However, we are
|
|
building a system for which a prime goal is the reading and
|
|
investigation of machine-readable documents on the web. We use
|
|
the URI log:semantics for this function and apologize for any
|
|
heartache it may cause.]<br />
|
|
<br />
|
|
<br />
|
|
|
|
<p><a name="includes" id="includes"> F = G iff |stF|
|
|
= |stG| and there is some substitution σ such
|
|
that (∀<span style="font-style: italic;">i</span>
|
|
. ∃<span style="font-style: italic;">j</span> .
|
|
σ<span style="font-style: italic;">Fi</span> =
|
|
σG<span style=
|
|
"font-style: italic;">j. </span>)</a></p>
|
|
|
|
<p><a name="includes" id="includes"></a></p>
|
|
|
|
<h2><a name="includes" id="includes">Appendix: Colophon</a></h2>
|
|
|
|
<p><a name="includes" id="includes">formatting XHTML 1 with
|
|
nvu</a></p>
|
|
|
|
<h2><a name="includes" id="includes">Appendix: Drafting
|
|
Notes</a></h2>
|
|
|
|
<p><a name="includes" id="includes">yes, discuss notational
|
|
abbreviation, but not abstract syntax</a></p>
|
|
|
|
<p><a name="includes" id="includes">hmm... are log:includes,
|
|
log:implies and such predicates? relations? operators?
|
|
properties?</a></p>
|
|
|
|
<p><a name="includes" id="includes">To do: describe the syntactic
|
|
sugar transformations formally to close the loop.</a></p>
|
|
</body>
|
|
</html>
|