--- a/semantics/prov-sem.html Thu Apr 11 15:35:51 2013 +0100
+++ b/semantics/prov-sem.html Thu Apr 11 15:38:16 2013 +0100
@@ -991,7 +991,7 @@
<p> This document presents a model-theoretic semantics for the PROV
-data model (called the <dfn>naive semantics</dfn>), viewing
+data model, viewing
PROV-DM statements as atomic formulas in the sense of first-order
logic, and viewing the constraints and inferences specified in
PROV-CONSTRAINTS as a first-order theory. It is shown that valid PROV
@@ -1053,7 +1053,7 @@
[[PROV-CONSTRAINTS]] that
specifies definitions, inferences, and constraints that can be used to
reason about PROV documents, or determine their validity. This document
-provides a naive formal semantics of PROV, providing a formal
+provides a formal semantics of PROV, providing a formal
counterpart to the informal descriptions and motivations given
elsewhere in PROV specifications.</p>
@@ -1107,14 +1107,14 @@
instances correspond to satisfiable theories: every valid instance has
a model, and vice versa.</p>
-<p> The <a>naive semantics</a> has some appealing
+<p> The semantics has some appealing
properties. Specifically, it provides a declarative counterpart to
the operational definition of validity taken in PROV-CONSTRAINTS. In
the specification, validity is defined via a normalization process
followed by constraint checking on the normal form. This approach was adopted
to keep the specification closer to implementations, although other
implementations are possible and allowed. In addition to providing a
-<a>naive semantics</a>, this document shows that the operational
+semantics, this document shows that the operational
presentation of PROV validity checking is equivalent to the
declarative presentation adopted here. This could help justify
alternative approaches to validity checking.</p>
@@ -1161,7 +1161,7 @@
<li><a href="#soundness-completeness">Section 6</a> summarizes the
main results relating PROV-CONSTRAINTS validation to the semantics,
including soundness and a weak form of completeness: a PROV
- instance is valid if and only if it has a naive model.</li>
+ instance is valid if and only if it has a model.</li>
</ul>
@@ -1275,7 +1275,7 @@
<p>Restricting attention to linearly-ordered times, and imposing this
order on events, is a simplifying assumption; it is more restrictive than required to model the
constraints. As a result, there are currently some valid PROV
- instances that do not have naive models. It is intended that the
+ instances that do not have models. It is intended that the
final version of the semantics will provide a more general class of
models such that every valid instance has a model.
</p>
@@ -2736,7 +2736,7 @@
In this section we restate all of the inferences and constraints
of PROV-CONSTRAINTS in terms of first-order logic. For each, we
give a proof sketch showing why the inference or constraint is
- sound for reasoning about the <a>naive semantics</a>. We exclude the
+ sound for reasoning about the semantics. We exclude the
definitional rules in PROV-CONSTRAINTS because they are only
needed for expanding the abbreviated forms of PROV-N statements to
the logical formulas used here.</p>
@@ -3846,7 +3846,7 @@
<h2>Soundness and Completeness</h2>
<p>Above we have presented arguments for the soundness of the
-constraints and inferences with respect to the <a>naive semantics</a>.
+constraints and inferences with respect to the semantics.
Here, we relate the notions of <dfn>validity</dfn> and <dfn>normal
form</dfn> defined in PROV-CONSTRAINTS to the semantics.
</p>
--- a/semantics/releases/NOTE-prov-sem-20130430/Overview.html Thu Apr 11 15:35:51 2013 +0100
+++ b/semantics/releases/NOTE-prov-sem-20130430/Overview.html Thu Apr 11 15:38:16 2013 +0100
@@ -747,7 +747,7 @@
div.MathJax_MathML {display: block}
.MathJax_mmlExBox {display: block; overflow: hidden; height: 1px; width: 60ex; padding: 0; border: 0; margin: 0}
</style><!--[if lt IE 9]><script src='http://www.w3.org/2008/site/js/html5shiv.js'></script><![endif]--></head>
- <body><div class="head">
+ <body><div id="MathJax_Message" style="display: none; "></div><div class="head">
<p>
<a href="http://www.w3.org/"><img width="72" height="48" src="http://www.w3.org/Icons/w3c_home" alt="W3C"></a>
@@ -804,7 +804,7 @@
<hr>
-</div><div id="MathJax_Message" style="display: none; "></div>
+</div>
<section id="abstract" class="introductory"><h2>Abstract</h2>
<p>
@@ -817,7 +817,7 @@
<p> This document presents a model-theoretic semantics for the PROV
-data model (called the <dfn id="dfn-naive-semantics">naive semantics</dfn>), viewing
+data model, viewing
PROV-DM statements as atomic formulas in the sense of first-order
logic, and viewing the constraints and inferences specified in
PROV-CONSTRAINTS as a first-order theory. It is shown that valid PROV
@@ -932,7 +932,7 @@
[<cite><a class="bibref" href="#bib-PROV-CONSTRAINTS">PROV-CONSTRAINTS</a></cite>] that
specifies definitions, inferences, and constraints that can be used to
reason about PROV documents, or determine their validity. This document
-provides a naive formal semantics of PROV, providing a formal
+provides a formal semantics of PROV, providing a formal
counterpart to the informal descriptions and motivations given
elsewhere in PROV specifications.</p>
@@ -986,14 +986,14 @@
instances correspond to satisfiable theories: every valid instance has
a model, and vice versa.</p>
-<p> The <a href="#dfn-naive-semantics" class="internalDFN">naive semantics</a> has some appealing
+<p> The semantics has some appealing
properties. Specifically, it provides a declarative counterpart to
the operational definition of validity taken in PROV-CONSTRAINTS. In
the specification, validity is defined via a normalization process
followed by constraint checking on the normal form. This approach was adopted
to keep the specification closer to implementations, although other
implementations are possible and allowed. In addition to providing a
-<a href="#dfn-naive-semantics" class="internalDFN">naive semantics</a>, this document shows that the operational
+semantics, this document shows that the operational
presentation of PROV validity checking is equivalent to the
declarative presentation adopted here. This could help justify
alternative approaches to validity checking.</p>
@@ -1040,7 +1040,7 @@
<li><a href="#soundness-completeness">Section 6</a> summarizes the
main results relating PROV-CONSTRAINTS validation to the semantics,
including soundness and a weak form of completeness: a PROV
- instance is valid if and only if it has a naive model.</li>
+ instance is valid if and only if it has a model.</li>
</ul>
@@ -1154,7 +1154,7 @@
<p>Restricting attention to linearly-ordered times, and imposing this
order on events, is a simplifying assumption; it is more restrictive than required to model the
constraints. As a result, there are currently some valid PROV
- instances that do not have naive models. It is intended that the
+ instances that do not have models. It is intended that the
final version of the semantics will provide a more general class of
models such that every valid instance has a model.
</p>
@@ -2611,7 +2611,7 @@
In this section we restate all of the inferences and constraints
of PROV-CONSTRAINTS in terms of first-order logic. For each, we
give a proof sketch showing why the inference or constraint is
- sound for reasoning about the <a href="#dfn-naive-semantics" class="internalDFN">naive semantics</a>. We exclude the
+ sound for reasoning about the semantics. We exclude the
definitional rules in PROV-CONSTRAINTS because they are only
needed for expanding the abbreviated forms of PROV-N statements to
the logical formulas used here.</p>
@@ -3716,7 +3716,7 @@
<!--OddPage--><h2><span class="secno">6. </span>Soundness and Completeness</h2>
<p>Above we have presented arguments for the soundness of the
-constraints and inferences with respect to the <a href="#dfn-naive-semantics" class="internalDFN">naive semantics</a>.
+constraints and inferences with respect to the semantics.
Here, we relate the notions of <dfn id="dfn-validity">validity</dfn> and <dfn id="dfn-normal-form">normal
form</dfn> defined in PROV-CONSTRAINTS to the semantics.
</p>
Binary file semantics/releases/NOTE-prov-sem-20130430/prov-sem.pdf has changed