From d1ae01619b9704dafaf1e07793a5f6c979629202 Mon Sep 17 00:00:00 2001 From: doerthe Date: Mon, 3 Nov 2025 15:11:46 +0100 Subject: [PATCH 1/3] adapting proofs for interpolation lemma and canonical model --- spec/index.html | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/spec/index.html b/spec/index.html index fed12ff..c2546ff 100644 --- a/spec/index.html +++ b/spec/index.html @@ -1913,8 +1913,9 @@

Proofs of some results

Every graph is simply satisfiable.

-

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

- +

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

+

G simply entails a graph E if and only if a subgraph of G is an instance of E.

@@ -1922,8 +1923,8 @@

Proofs of some results

If a subgraph 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 Herbrand interpretation I of G defined as follows. - IR contains the names and blank nodes which occur in the graph, with I(n)=n - for each name n; n is in IP and <a, b> in IEXT(n) just when the triple <a n b> is in the graph. + IR contains the names, triple terms and blank nodes which appear in the graph, with I(n)=n + for each name n and IT(s,p,o)=<s,p,o>; n is in IP and <a, b> in IEXT(n) just when the triple <a n b> is in the graph. (For IRIs which do not occur in the graph, assign them values in IR at random.) I satisfies every triple <s p o> in E; that is, for some mapping A from the blank nodes of E to the vocabulary of G, From af9504b7ac9dfeaa98f39110ce644c278ad0e170 Mon Sep 17 00:00:00 2001 From: Enrico Franconi Date: Thu, 6 Nov 2025 11:09:01 +0900 Subject: [PATCH 2/3] added oxford comma Co-authored-by: Ted Thibodeau Jr --- spec/index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/index.html b/spec/index.html index c2546ff..10a1d91 100644 --- a/spec/index.html +++ b/spec/index.html @@ -1923,7 +1923,7 @@

Proofs of some results

If a subgraph 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 Herbrand interpretation I of G defined as follows. - IR contains the names, triple terms and blank nodes which appear in the graph, with I(n)=n + IR contains the names, triple terms, and blank nodes which appear in the graph, with I(n)=n for each name n and IT(s,p,o)=<s,p,o>; n is in IP and <a, b> in IEXT(n) just when the triple <a n b> is in the graph. (For IRIs which do not occur in the graph, assign them values in IR at random.) I satisfies every triple <s p o> in E; that is, From 6b56360e1d02d8ca790dc6dcd8cb0a6195ea2448 Mon Sep 17 00:00:00 2001 From: Enrico Franconi Date: Thu, 6 Nov 2025 11:12:15 +0900 Subject: [PATCH 3/3] oxford comma + just -> only Co-authored-by: Ted Thibodeau Jr --- spec/index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/index.html b/spec/index.html index 10a1d91..2dca40f 100644 --- a/spec/index.html +++ b/spec/index.html @@ -1924,7 +1924,7 @@

Proofs of some results

so G entails E. Now suppose G entails E, and consider the Herbrand interpretation I of G defined as follows. IR contains the names, triple terms, and blank nodes which appear in the graph, with I(n)=n - for each name n and IT(s,p,o)=<s,p,o>; n is in IP and <a, b> in IEXT(n) just when the triple <a n b> is in the graph. + for each name n and IT(s,p,o)=<s,p,o>; n is in IP and <a, b> is in IEXT(n), only when the triple <a n b> is in the graph. (For IRIs which do not occur in the graph, assign them values in IR at random.) I satisfies every triple <s p o> in E; that is, for some mapping A from the blank nodes of E to the vocabulary of G,