Skip to content

Updating Appendix B (used to be C): Proofs for some results #165

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Nov 11, 2025
Merged

Updating Appendix B (used to be C): Proofs for some results #165

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d1ae016
adapting proofs for interpolation lemma and canonical model
doerthe Nov 3, 2025
af9504b
added oxford comma
franconi Nov 6, 2025
6b56360
oxford comma + just -> only
franconi Nov 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions spec/index.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1913,17 +1913,18 @@ <h2>Proofs of some results</h2>

<p class="fact">Every graph is simply <a>satisfiable</a>.</p>

<p>Consider the simple interpretation with universe {x}, IEXT(x)= &lt;x,x &gt; and I(aaa)=x for any IRI aaa. This interpretation satisfies every RDF graph. QED.</p>

<p>Consider the simple interpretation with universe {x} union all (abstract) triple terms which can be formed from x,
IEXT(x)= &lt;x,x&gt;, IS(aaa)=x, IL(aaa) = x, IT(yyy,x,zzz) = &lt;yyy,x,zzz&gt;, for any term aaa and any elements of the domain of discourse yyy and zzz. This interpretation satisfies every RDF graph. QED.</p>

<p class="fact">
G <a>simply entails</a> a graph E if and only if a <a>subgraph</a> of G is an instance of E.
</p>

<p>If a <a>subgraph</a> E' of G is an instance of E then G entails E' which entails E,
so G entails E. Now suppose G entails E, and consider the
<a href="http://en.wikipedia.org/wiki/Herbrand_interpretation">Herbrand interpretation</a> I of G defined as follows.
IR contains the <a>names</a> and blank nodes which occur in the graph, with I(n)=n
for each <a>name</a> n; n is in IP and &lt;a, b&gt; in IEXT(n) just when the triple &lt;a n b&gt; is in the graph.
IR contains the <a>names</a>, triple terms, and blank nodes which appear in the graph, with I(n)=n
for each <a>name</a> n and IT(s,p,o)=&lt;s,p,o&gt;; n is in IP and &lt;a, b&gt; is in IEXT(n), only when the triple &lt;a n b&gt; is in the graph.
(For IRIs which do not occur in the graph, assign them values in IR at random.)
I <a>satisfies</a> every triple &lt;s p o&gt; in E; that is,
for some mapping A from the blank nodes of E to the vocabulary of G,
Expand Down
Loading