% $Id: RDFCoreMT.lsl,v 1.5 2003/01/31 14:51:05 connolly Exp $ % % Model theory for RDF, developed by the RDF Core WG % % cf "updated draft of model theory" Pat hayes Jul 27 2001 RDFCoreMT: trait includes RDFAbSyn, Set(Blank_node, FiniteSet[Blank_node] for Set[E]), Set(URI_reference, Vocabulary for Set[E]), % finite Set(Graph, FiniteSet[Graph] for Set[E]), % finite RelSet(Resource, Set[Resource]), RelSet(Pair[Resource], Set[Pair[Resource]]), FiniteMap(Blank_node, Resource) Pair[Resource] tuple of x, y: Resource introduces % 0.3 Graph Definitions subgraph: Graph, Graph -> Bool merge: FiniteSet[Graph] -> Graph triples: FiniteSet[Graph] -> Graph rename: Graph, FiniteSet[Blank_node] -> Graph rename: Term, FiniteSet[Blank_node] -> Term noSharedBnodes: FiniteSet[Graph] -> Bool % ground bnodes: Term -> FiniteSet[Blank_node] bnodes: triple -> FiniteSet[Blank_node] bnodes: Graph -> FiniteSet[Blank_node] bnodes: FiniteSet[Graph] -> FiniteSet[Blank_node] ground: Graph -> Bool % vocabulary urirefs: Term -> Vocabulary urirefs: triple -> Vocabulary vocabulary: Graph -> Vocabulary % @@names... do we need this? instance: Graph, Graph -> Bool % @@ proper instance, instance w.r.t. a vocab %%%%%%%%%%%%%%%%% % 1.3 Interpretations LV : -> Set[Resource] asResource: Term -> Resource % the herberand trick __ [ __ ] : Interpretation, Vocabulary -> InterpOfVocab %@@generated by? tuple of? IR: InterpOfVocab -> Set[Resource] % domain IP: InterpOfVocab -> Set[Resource] % IP IEXT: InterpOfVocab, Resource -> Set[Pair[Resource]] IS: InterpOfVocab, URI_reference -> Resource IL: InterpOfVocab, Literal -> Resource % only typed literals specified... hmm... % 1.4 Denotations of ground graphs __ [ __ ] : InterpOfVocab, Term -> Resource __ [ __ ] : InterpOfVocab, triple -> Bool __ [ __ ] : InterpOfVocab, Graph -> Bool % @@hmm... is it the case that this trait 'converts', in % the larch sense, these last two? i.e. is interpretation % of triples ans sets of triples defined relative % to interpretation of terms and IEXT? % 1.5. Blank nodes as existential assertions __ + __ : InterpOfVocab, Map[Blank_node, Resource] -> InterpOfVocab %%%%%%%%%%%%%%%% % 2. Simple entailment between RDF graphs satisfies : InterpOfVocab, Graph -> Bool entails: FiniteSet[Graph], Graph -> Bool % @@skipping valid/invalid... asserts % 0.3 Graph Definitions forall ts1, ts2: Graph, b: Blank_node, i1: URI_reference, l1: Literal, bs1: FiniteSet[Blank_node], s, p, o: Term, spo: triple, g1: Graph, S: FiniteSet[Graph], s1: UnicodeStringInNormalFormC, lo1: Opt[Language_Identifier], m: Map[Blank_node, Term] ts1 \subseteq ts2 <=> subgraph(ts1, ts2); bnodes(blank(b)) = {b}; bnodes(uref(i1)) = {}; bnodes(lit(l1)) = {}; bnodes([s, p, o]) = bnodes(s) \U bnodes(p) \U bnodes(o); bnodes({}:Graph) = {}; bnodes(insert(spo, ts1)) = bnodes(ts1) \U bnodes(spo); bnodes({}:FiniteSet[Graph]) = {}; bnodes(insert(ts1, S)) = bnodes(ts1) \U bnodes(S); merge({}) = {}; noSharedBnodes(S) => ( merge(insert(ts1, S)) = rename(ts1, bnodes(S)) ); noSharedBnodes({}); noSharedBnodes(S) /\ (bnodes(ts1) \I bnodes(S) = {}) => noSharedBnodes(insert(ts1, S)); rename({}, bs1) = {}; rename(insert([s, p, o], ts1), bs1) = insert([rename(s, bs1), rename(p, bs1), rename(o, bs1)], ts1); rename(uref(i1), bs1) = uref(i1); rename(lit(l1), bs1) = lit(l1); tag(rename(blank(b), bs1)) = blank; rename(blank(b), bs1).blank \notin bs1; % we assume there are plenty of bnodes ground(g1) <=> bnodes(g1) = {}; urirefs(blank(b)) = {}; urirefs(uref(i1)) = {i1}; urirefs(lit([s1, lo1, value(i1)])) = {i1}; urirefs(lit([s1, lo1, absent(nil)])) = {}; urirefs([s, p, o]) = urirefs(s) \U urirefs(p) \U urirefs(o); vocabulary({}) = {}; vocabulary(insert(spo, ts1)) = vocabulary(ts1) \U urirefs(spo); (m[ts1] = ts2) => subgraph(ts2, ts1); forall I: Interpretation, V: Vocabulary, i: URI_reference, l1: Literal, p1, r1, r2: Resource % IR superset LV LV \subseteq IR(I[V]); plain(l1) => asResource(lit(l1)) \in LV; % domain, IR is not empty IR(I[V]) ~= {}; IP(I[V]) \subseteq IR(I[V]); [r1, r2] \in IEXT(I[V], p1) => (p1 \in IP(I[V]) /\ r1 \in IR(I[V]) /\ r2 \in IR(I[V]) ); (i \in V) <=> (IS(I[V], i) \in IR(I[V])); % range of IL is typed literals only IL(I[V], l1) \in IR(I[V]) => typed(l1); % 1.4 Denotations of ground graphs forall l1: Literal, i1: URI_reference, I: InterpOfVocab, s, p, o: Term, ts1: Graph, ep: triple plain(l1) => (I[lit(l1)] = asResource(lit(l1))); typed(l1) => (I[lit(l1)] = IL(I, l1)); (I[uref(i1)] = IS(I, i1)); I[[s, p, o]] <=> [I[s], I[o]] \in IEXT(I, I[p]); ground(ts1) => (not(I[ts1]) <=> (\E ep (ep \in ts1 /\ not(I[ep])))); %@@ some theorems we could check: % "If the vocabulary of an RDF graph contains urirefs that are not in the vocabulary of an interpretation I - that is, if I simply does not give a semantic value to some name that is used in the graph - then these truth-conditions will always yield the value false for some triple in the graph, and hence for the graph itself. Turned around, this means that any assertion of a graph implicitly asserts that all the names in the graph actually refer to something in the world." % "The final condition implies that an empty graph (an empty set of triples) is trivially true." % 1.5. Blank nodes as existential assertions forall I: InterpOfVocab, A: Map[Blank_node, Resource], b: Blank_node, g: Graph (I+A)[blank(b)] = apply(A, b); (I)[g] <=> \E A ((I+A)[g]); %%%%%%%%%%%%%%%% % 2. Simple entailment between RDF graphs forall I: InterpOfVocab, E, es: Graph, S: FiniteSet[Graph] satisfies(I, E) <=> I[E]; entails(S, E) <=> (\A I ((\A es (es \in S => satisfies(I, es))) => satisfies(I, E))); implies forall I: InterpOfVocab, E, sg: Graph, S: FiniteSet[Graph] % Interpolation Lemma. entails(S, E) <=> \E sg (subgraph(sg, merge(S)) /\ instance(sg, E));