Unify triples and triple terms at the end of 5.3

* First version of liberal semantics - it lack the entailment pattern for rdfs:Proposition

* Missing fix to rdfs14

* liberal baseline RDF and RDFS semantics

* Fixed HTML + RTD -> RDF

* Fixed more HTML

* Minor fix in text for better English

Co-authored-by: Ted Thibodeau Jr <[email protected]>

* Better English: added comma

* Added axiomatic triple in RDF for rdf:reifies

* Moved the "appears in" definition before its first use.

* "RDF term" definition is exported

Co-authored-by: Pierre-Antoine Champin <[email protected]>

* Added the reference to RTDF symmetric triple

* Changed rdf:range to rdfs:range

Co-authored-by: Niklas Lindström <[email protected]>

* Replaced [I+A] with I for rdf/rdfs namespace IRIs

* Better spacing

Co-authored-by: Ted Thibodeau Jr <[email protected]>

* Better formatting of rdfssemcond11 definition.

* Fixed a plural reference

Co-authored-by: Ted Thibodeau Jr <[email protected]>

* Fixed redundant condition "triple or triple term"

* Fixed wording of rdfs14, and references to issue about external references and completeness proof

* Better rdfs14

* Added example for rdfs14

* Change: emdashes are better than the colons

Co-authored-by: Ted Thibodeau Jr <[email protected]>

* Small typo in index.html

* fixed: emdash written as mdash

* Added semantic properties in 5.3 relating triple terms and asserted triples

* Better formatting

Co-authored-by: Niklas Lindström <[email protected]>

* Rewording after suggestion of pfps

* Minor wording fixed as per comments in PR, plus rewording of general definition of satisfiability as suggested by Doerthe

* Update index.html

Minor fix

* Added RE to the definition of propositions and facts

Co-authored-by: Niklas Lindström <[email protected]>

* Fixed a missing RE

Co-authored-by: Niklas Lindström <[email protected]>

* Fixed the observation of IPR

Co-authored-by: Niklas Lindström <[email protected]>

* Text fix in FEXT definition

Co-authored-by: Ted Thibodeau Jr <[email protected]>

---------

Co-authored-by: Ted Thibodeau Jr <[email protected]>
Co-authored-by: Pierre-Antoine Champin <[email protected]>
Co-authored-by: Niklas Lindström <[email protected]>
Co-authored-by: doerthe <[email protected]>

Author: 5 people

spec/index.html

@@ -410,7 +410,7 @@ <h2>Simple Interpretations</h2>
               set of sets of pairs &lt; x, y &gt; with x and y in IR .</p>
         <p>4. A mapping IS from IRIs into (IR union IP)</p>
         <p>5. A partial mapping IL from literals into IR </p>
-        <p>6. An injective mapping RE from IR x IP x IR into IR, called the interpretation of triple terms. </p>
+        <p>6. An injective mapping RE from IR x IP x IR into IR, called the denotation of triple terms. </p>
        </td>
     </tr>
   </table>
@@ -625,7 +625,7 @@ <h2>Simple Entailment</h2>
   </section>
 
   <section id="simple_entailment_properties" class="informative">
-    <h3>Properties of simple entailment (Informative)</h3>
+    <h3>Properties of simple entailment and satisfiability (Informative)</h3>
 
     <p>The properties described here apply only to simple entailment,
       not to extended notions of entailment introduced in later sections.
@@ -683,7 +683,25 @@ <h3>Properties of simple entailment (Informative)</h3>
 
     <p class="fact"> If E contains an IRI which does not occur anywhere in S,
       then S does not simply entail E.</p>
+      
+    <p>The following semantic properties relate triple terms and triples asserted in a graph, and they introduce a general definition of satisfiability.</p>
+    
+    <p>We define the <dfn>set of propositions</dfn> in an interpretation as follows:</p>
+
+	<p class="fact"> The set of propositions in an interpretation I is IPR(I) = {&nbsp;RE(x, y, z)&#65372;x is in IR, y is in IP, z is in IR&nbsp;}; we observe that a proposition is in the extension of <code>rdfs:Proposition</code>. </p>
+
+	<p>We define the <dfn>set of facts</dfn> in an interpretation as follows:</p>
+
+	<p class="fact"> The set F of facts in an interpretation I is F(I) = {&nbsp;RE(x, y, z)&#65372;&lt;x, z&gt; is in IEXT(y)&nbsp;}. The set of facts is the set of propositions which are true in the interpretation. </p>
+
+	<p>Given a blank node mapping, we define the <dfn>set of facts asserted by a graph</dfn> in an interpretation as follows:</p>
+
+	<p class="fact">Given a blank node mapping A, the set of all facts asserted by a graph G in an interpretation I is FEXT(G, I, A) = {&nbsp;RE(&nbsp;[I+A](s), I(p), [I+A](o)&nbsp;)&#65372;`s p o.` is in G&nbsp;}. We then observe that given a blank node mapping, the asserted facts of a graph with respect to an interpretation may not necessarily be among the facts of the interpretation.</p>
+	
+	<p>We introduce a <dfn>general definition of satisfiability</dfn> of a graph in an interpretation as follows:</p>
 
+	<p class="fact">An interpretation (simply) satisfies a graph if and only if there exists a blank node mapping such that the facts asserted by the graph in the interpretation are among the facts of the interpretation.</p>
+	
   </section>
 </section>