author | jcheney@inf.ed.ac.uk |

Thu, 11 Apr 2013 15:38:16 +0100 | |

changeset 6131 | 77dfd95854c9 |

parent 6130 | 3edb9a029518 |

child 6132 | 24872954205c |

* re-staged

semantics/prov-sem.html | ||

semantics/releases/NOTE-prov-sem-20130430/Overview.html | ||

semantics/releases/NOTE-prov-sem-20130430/prov-sem.pdf |

--- 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>