Checking and updating Appendix C "Proofs of some results"

[franconi]

Proofs to be updated to hold for RDF 1.2.
Assigned to @doerthe .

[pfps]

I see two changes needed:

Lemma: Every graph is simply satisfiable.

Consider the simple interpretation with universe {x} union the set of triple terms union { n }, IEXT(x)= <x,x>, IS(aaa)=x, IL(l) = n, IT(<aaa,bbb,ccc>) = <aaa,bbb,ccc>, for any IRI aaa. This interpretation satisfies every RDF graph. QED.

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

WAS:

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 is in the graph. (For IRIs which do not occur in the graph, assign them values in IR at random.) I satisfies every triple in E; that is, for some mapping A from the blank nodes of E to the vocabulary of G, the triple <I+A I(p) I+A> occurs in G. But this is an instance of under the instance mapping A; so an instance of E is a subgraph of G. QED.

CHANGE to Enrico's proof.