We study constraints for RDF-Schema (RDFS) graphs. The syntax and semantics is de ned for constraints in graphs that can contain RDFS properties and blank nodes. The proposal for constraint satisfaction closely resembles the possible world approach found in various contexts of incomplete databases and knowledge bases. Positive decidability results for checking satisfaction of RDFS constraints under blank nodes are given. In addition, we present deductive rules for di erent kinds of constraints and for several combination of them. Our approach resembles similar deductive rules of relational database contexts, but they are generalized and adapted to the RDFS data model using homomorphisms and embeddings.
RDF (Resource Description Framework) [
RDF-graphs convey information about a certain domain under consideration. As with any other data format, in order to specify conditions that must be satis ed by an RDF-graph, constraints need to be imposed. In practical settings, constraints are commonly used for three main tasks: specifying properties of the data itself; handle contradictions within the database or with respect to the domain under consideration; or as a help for semantic query optimizations.
In recent years, important progress has been made towards extending the
basic RDF framework with constraints. To the best of our knowledge, the proposals
so far, however, exclude the use of RDFS properties. This simpli cation restricts
the usability of such constraints in real world domains, where the use of RDFS
coupled with blank nodes is common practice. Hence, one speci c goal of this
paper is to tackle this issue by extending the semantics of the RDF constraints
introduced in [
In general terms, this paper is an e ort towards a general theory of reasoning with constraints in RDF. The concrete contributions of this paper are as follows. 1. We de ne the semantics of several types of constraints for RDFSgraphs with schema properties and blank nodes; 2. We present a number of decidability results concerning the satisfaction of constraints under blank nodes in RDFS-graphs; 3. We provide sound and complete deductive rules for di erent kinds of constraints and for several combination of them; and 4. We study how RDFS properties can be expressed by a number of additional triple generating constraints. We deal with subclass, type, subproperty, domain and range.
This paper is organized as follows. In Section 2 we introduce the basic terminology and preliminary de nitions we use throughout the paper. In Section 3 we study decidability problems on RDF constraints satisfaction and entailment. In Section 4, we extend our framework to RDFS graphs. Related work is surveyed in Section 5, which also contains our conclusions. 2
In what follows, we use the following vocabulary:
V , an in nite set of variables denoted by pre xing them by $;
A homomorphism from a set of triples of terms S in a set of triples of terms S0 is a total function1 h : VS [ US ! VS0 [ US0 , such that h(u) = u, for each u 2 US ;
If (t1; t2; t3) 2 S then (h(t1); h(t2); h(t3)) 2 S0; De nition 1 (RDF-graph). An RDF-graph (or graph) G is a nite set of triples (s; p; o), subject, property, object, s; o 2 U [B, p 2 U . A graph is grounded if it does not contain blank nodes.
De nition 2 (Grounding). A grounding of a graph G, is a total function : BG [ UG ! U , where (u) = u, for u 2 UG . The grounded graph G of G under is de ned as G = f( (t1); (t2); (t3)) j (t1; t2; t3) 2 Gg. The set of grounded graphs of a graph G is denoted
GG = fG j
is a grounding of Gg: 1 h is not necessary a surjection. Note that a grounded graph does not contain blank nodes and that every grounded graph is a graph with only one grounding, i.e. the identity.
De nition 3 (Embedding of a set of triples of terms in G ). An embedding of a nite set S of triples of terms in a graph G is a total function e : VS [ US ! U 2, such that e(u) = u, for each u 2 U ;
If (t1; t2; t3) 2 S then (e(t1); e(t2); e(t3)) 2 G . 3
In this section we discuss four types of RDF-constraints: Equality Generating, Functional, Triple Generating and Forbidding Constraints.
In general an RDF-constraint is a condition which a graph can satisfy or not.
of GG satisfy C3. We denote that a graph G satis es an RDF-constraint C as G j= C. 3.1
Types of Constraints
In [
E is a nite set of equalities, each of the form (t1 = t2), with t1; t2 2 VS [ U . A grounded graph G satis es the EGC (S; E) i for every embedding e of S in G, and every (t1 = t2) 2 E holds that e(t1) = e(t2).
Example 1. Consider the constraint C1 = (f($x; a; $y)g; f($x = $y)g). f(b; b; c); (b; b; a)g j= C1 f( a; a; c); (b; a; a)g 6j= C1 f( a; a; b); ( b; a; b)g 6j= C1 f( a; b; b); ( a; b; c)g j= C1.
In a similar way as with EGCs, we proceed with de ning functional constraints.
S is a nite set of triples of terms;
L; R VS . 2 We denote US (resp. BS and VS) for the set of elements of U (resp. B and V ) that occur in S. 3 The notion of satisfaction for grounded graphs is separately de ned below for each type of constraint. A grounded graph G satis es the FC (S; L ! R) i for every two embeddings of S in G that coincide4 on the variables of L, they also coincide on the variables of R.
Example 2. Consider the constraint C2 = (f($x; a; $y)g; f$xg ! f$yg). f(b; b; c); (b; b; a)g j= C2 f( a; a; c); (b; a; a)g 6j= C2 f( a; a; b); ( b; a; b)g j= C2 f( a; b; b); ( a; b; c)g j= C2.
In [
Lemma 1. A functional constraint can be expressed in terms of equality generating constraints.
De nition 6 (TGC). A triple generating constraint is a pair (S; S0), where S and S0 are both nite sets of triples of terms and VS0 VS . A grounded graph G satis es the TGC (S; S0) if every embedding e of S in G is also an embedding of S0 in G.
Example 3. Consider the constraint C3 = (f($x; a; $y)g; f($y; a; $x)g).
f(b; a; c); (c; a; b)g j= C3 f( a; a; c); (c; a; b)g 6j= C3.
While EGCs, FCs and TGCs require properties for all possible embeddings, forbidding constraints forbid some embeddings.
De nition 7 (FBC). A forbidding constraint has the form (S), where S is a nite set of triples of terms. A grounded graph G satis es the FBC (S) i there is no embedding of S in G.
Example 4. Consider C4 = (f($x; a; $x)g) f(b; a; b)g 6j= C4 f( a; b; c)g j= C4.
f(a; b; a)g j= C4 Since there is a nite number of embeddings of a grounded graph, by Lemma 1 we can easily prove nite set of triples into a Theorem 1. It is decidable whether a grounded graph G satis es an EGC (S; E), an FC (S; L ! R), a TGC (S; S0) or a FBC (S).
Let SC be a nite set of constraints and C be a constraint, we say that C is a logical grounded consequence of SC i for all grounded graphs G holds 4 Two embeddings e and e0 coincide on a variable $v i e($v) = e0($v). 3.2
Logical Grounded Consequences Theorem 2. Given a nite set E of EGCs. It is decidable whether an EGC (S; E) is a logical grounded consequence of E.
By Lemma 1 and Theorem 2 we have Theorem 3. Given a nite set F of FCs. It is decidable whether an FC (S; L ! R) is a logical grounded consequence of F .
Theorem 4. Given a nite set T of TGCs. It is decidable whether a TGC (S; S0) is a logical grounded consequence of T .
Proof. Initialize the graph S as S where each variable $x is substituted by a new
Theorem 5. Given a nite set F B of FBCs. It is decidable whether an FBC (S) is a logical grounded consequence of F B.
Proof. Consider the graph S as S where each variable $x is substituted by a new URI x. 9(S0) 2 F B with S j= (S0) i (S) is a logical grounded consequence of F B.
more logical grounded EGC consequences than E. Indeed, (f(a; $x; $y)g; f($y =
f(a; a; $y)g); (f(a; a; $y)g; f($y = a)g)g but not of f(f(a; a; $y)g; f($y = a)g)g.
Theorem 6. Given a nite set T E of TGCs and EGCs. It is decidable whether a TGC (S; S0) is a logical grounded consequence of T E. It is decidable whether an EGC (S; E) is a logical grounded consequence of T E.
Theorem 7. Given a nite set T F B of TGCs and FBCs. It is decidable whether a TGC (S; S0) is a logical grounded consequence of T F B. It is decidable whether a FBC (S) is a logical grounded consequence of T F B. 3.3
Deductive Rules for Grounded Graphs Next we are giving a sound, independent and complete set of deductive rules for grounded graphs. A set of deductive rules de nes when SC ` C, with SC is a set of constraints and C a constraint. We prove each time that
SC ` C ) 8GG((8C0 2 SC(GG j= C0)) ) GG j= C); soundness SC ` C ( 8GG((8C0 2 SC(GG j= C0)) ) GG j= C); completeness
where GG are grounded graphs and the subscript r means \without using Rule r".
for EGCs Rules E0-E8 is proved to be sound, independent and complete for grounded graphs: Rule E0 : E ` (S; E), for every (S; E) 2 E ; Rule E1 : E ` (S; f(t = t)g), for every nite set S of triples of terms and t 2 VS [ US ; Rule E2 : E ` (S; f(t1 = t2)g) implies E ` (S; f(t2 = t1)g); Rule E3 : E ` (S; f(t1 = t2); (t2 = t3)g) implies E ` (S; f(t1 = t3)g); Rule E4 : E ` (S; E) and E1 E implies E ` (S; E1); Rule E5 : E ` (S; E1) and E ` (S; E2) implies E ` (S; E1 [ E2);
(S1; h(E)); Rule E7 : E ` (S; f(t = t0)g) and E ` ( t -t0 (S); E) implies E ` (S; E); Rule E8 : E ` (S; f(a = b)g) for a; b 2 US and a 6= b implies E ` (S; E) for all possible E.
Theorem 8 ([
Theorem 9. Let T be a nite set of TGCs. The following set of deductive rules for TGCs is sound, independent and complete for grounded graphs: Rule T0 : (S; S0) 2 T implies T ` (S; S0); Rule T1 : T ` (S; S) for all S; Rule T2 : T ` (S0; S1) and T ` (S0; S2) implies T ` (S0; S1 [ S2); Rule T3 : T ` (S0; S1) and T ` (S0 [ S1; S2) implies T ` (S0; S2); Rule T4 : h is a homomorphism from S in S1 and T ` (S; S0) implies T ` (S1; h(S0)). Proof. Rules T0-T3 are clearly sound. For Rule T4, let G j= (S; S0) and let e be an embedding of S1 in G. Hence e h is an embedding of S in G, inducing that e h is also an embedding of S0 in G, concluding that e is an embedding of h(S0) in G.
Rules T0-T4 are complete. Indeed, referring to the proof of Theorem 4, we can deduce from Rules T0-T4 that T ` (S; S). Furthermore we have that T ` (S0; S1) and S2 S1 implies T ` (S0; S2), as a consequence of Rule T4. Rules T0-T4 are independent. We show this by giving for each 0 i 4 a set
T0 = f(f(a; b; c)g; f(d; e; f )g)g and T G0 = (f(a; b; c)g; f(d; e; f )g); T1 = f(f(a; b; c)g; f(d; e; f )g)g and T G1 = (f(g; h; i)g; ;); T2 = f(f(a; b; c)g; f(d; e; f )g); (f(a; b; c)g; f(g; h; i)g)g and T G2 = (f(a; b; c)g; f(d; e; f ); (g; h; i)g); T3 = f(f(a; b; c)g; f(d; e; f )g); (f(a; b; c); (d; e; f )g; f(g; h; i)g)g and T G3 = (f(a; b; c)g; f(g; h; i)g);
T4 = f(f(a; a; $x)g; f(a; $x; a)g)g and T G4 = (f(a; a; $y)g; f(a; $y; a)g); Lemma 2. 1. S1 S0 implies T ` (S0; S1); 2. T ` (S0; S1) and S0 S2 implies T ` (S2; S1); 3. T ` (S0; S1) and S2 S1 implies T ` (S0; S2).
Proof. 1. follows from Rule T4; 2. follows from Rule T4; 3. follows from 1., 2. and Rule T3.
Theorem 10. Let F B be a nite set of FBCs. The following set of deductive rules for FBCs is sound, independent and complete for grounded graphs: Rule FB0 : F B ` (S), for every (S) 2 F B; Rule FB1 : F B ` (S) and and h is a homomorphism from S in S1 implies F B ` (S1).
Proof. Sound: FB1. Let G j= F BC for all F BC 2 F B. So G j= (S) and there is no embedding e of S in G. If there would be an embedding e1 of S1 in G then e1 h would be an embedding of S in G. So G j= (S1).
Clearly FB0 and FB1 are independent.
clearly an embedding of S in the graph S. If there would be an (S0) 2 F B with an embedding e of S0 in S, there would be an homomorphism from S0 in S, implying that F B ` (S). Hence the graph S is a counterexample proving that (S) is not a logical grounded consequence of F B.
Theorem 11. Let T E be a nite set of TGCs and EGCs. The following set of deductive rules for TGCs and EGCs is sound, independent and complete for grounded graphs: Rules T0-T45; Rules E0-E86; Rule TE1 : T E ` (S; S0) and T E ` (S0; E) implies T E ` (S; E); Rule TE2 : T E ` (S; f(t = t0)g) and T E ` ( t -t0 (S); S0) implies T E ` (S; S0); Rule TE3 : T E ` (S; f(a = b)g) with a; b 2 US and a 6= b implies T E ` (S; S0) for all S0 with VS0 VS . (Proof, Cfr. Appendix.) Theorem 12. Let T F B be a nite set of TGCs and FBCs. The following set of deductive rules for TGCs and FBCs is sound, independent and complete for grounded graphs: Rules T0-T47; Rules FB0-FB18; Rule TFB0 : T F B ` (S; S0) and T F B ` (S0) implies F B ` (S); Rule TFB1 : T F B ` (S) implies T F B ` (S; S0) for every S0 with VS0 (Proof, Cfr. Appendix.) 3.4
Satis ability of Constraints for Graphs
Lemma 3. Let 1 and 2 be two isomorphic groundings of an RDF-graph G.
VS . 1(a) = 1. G 1 j= (S; E) i G 2 j= (S; E), with (S; E) an EGC; 2. G 1 j= (S; S0) i G 2 j= (S; S0), with (S; S0) an TGC; 3. G 1 j= (S) i G 2 j= (S), with (S) an FBC.
for each graph G and hence we have: Theorem 13. It is decidable whether a graph G satis es an EGC (S; E), an FC (S; L ! R), a TGC (S; S0) or a FBC (S).
The next theorem is straightforward consequence of Subsection 3.3: Theorem 14. Given a nite set SC of EGCs (resp. FCs, TGCs, FBCs). It is decidable whether an EGC (resp. FC, TGC, FBC) C is a logical consequence of SC. 5 Substitute T by T E 6 Substitute E by T E 7 Substitute T by T F B 8 Substitute F B by T F B Let us consider now sound, independent and complete sets of deductive rules for graphs. Clearly :
8GG((8C0 2 SC(GG j= C0)) ) GG j= C) , 8G((8C0 2 SC(G j= C0)) ) G j= C) where GG are grounded graphs and G are graphs.
Theorem 15. The set E0-E8 (resp. T0-T4, FB0-FB1 ) of deductive rules for EGCs (resp. TGCs, FBCs) is sound, independent and complete for graphs. The set E0-E8, T0-4, TE1-2 of deductive rules for EGCs and TGCs is sound, independent and complete for graphs.
The set FB0-1, T0-4, TFB0 of deductive rules for FBCs and TGCs is sound, independent and complete for graphs. 4 4.1
S-Constraints
An RDF Schema (abbreviated as RDFS) is an extensible knowledge
representation language providing basic elements for the description of ontologies, called
RDF vocabularies, intended to structure RDF-resources. The RDF-properties of
RDFS that we will consider are subproperty (sp), subclass (sc), typing (type),
domain (dom) and range (range). In the literature this fragment of RDFS is
called rdf [
De nition 8. An RDFS triple is a triple containing sp, sc, type, dom or range. An RDFS-graph is an RDF-graph that includes at least one RDFS triple. We will now express the semantics of RDFS-properties using triple generating constraints. We call the following set of TGCs, denoted by CS, S {Constraints. Consider the RDF-subjects or RDF-objects (that by the way can also be RDFproperties) S1, S2, S3, the RDF-properties P1, P2, P3, the classes of objects or subjects (or types) C1, C2 and C3.
Subproperty The RDFS subproperty is denoted by sp. (P1; sp; P2) indicates that P1 is a subproperty of P2. The semantics of sp says that if P1 is a subproperty of P2 and P2 is a subproperty of P3 then P1 is a subproperty of P3; this is expressed by the triple generating constraint:(f($p1; sp; $p2); ($p2; sp; $p3)g; f($p1; sp; $p3)g) if S1 has as property P1 with value S2 and P1 is a subproperty of P2 then S1 has also as property P2 with value S2, formally: (f($s1; $p1; $s2); ($p1; sp; $p2)g; f($s1; $p2; $s2)g) every property between a subject and an object is a subproperty of itself, formally: (f($s1; $p; $s2)g; f($p; sp; $p)g) if P1 is a subproperty of P2 then P1 and P2 are each a subproperty of itself, formally: (f($p1; sp; $p2)g; f($p1; sp; $p1); ($p2; sp; $p2)g) Subclass
of C2. The semantics of sc says that if C1 is a subclass of C2 and C2 is a subclass of C3 then C1 is a subclass of C3, formally:(f($c1; sc; $c2); ($c2; sc; $c3)g; f($c1; sc; $c3)g) if C1 is a subclass of C2 then C1 and C2 are each a subclass of itself, formally:(f($c1; sc; $c2)g; f($c1; sc; $c1); ($c2; sc; $c2)g)
Typing, Domain, Range The RDFS typing is denoted by type, the domain of a type by dom, its range by range. (S1; type; C1) indicates that C1 is a type of S1. (P1; dom; C1) indicates that C1 is the domain of P1. (P1; range; C1) indicates that C1 is the range of P1. Their semantics says that if C1 is a subclass of C2 and C1 is a type of S1 than C2 is also a type of S1, formally:(f($c1; sc; $c2); ($s1; type; $c1)g; f($s1; type; $c2)g) if C1 is the domain P1, and S1 has property P1, then C1 is a type of S1, formally:(f($p1; dom; $c1); ($s1; $p1; $s2)g; f($s1; type; $c1)g) if C1 is the range of the P1, and S2 is a value of the property P1, then C1 is a type of S1, formally:(f($p1; range; $c1); ($s1; $p1; $s2)g; f($s2; type; $c1)g) if C1 is the domain of P1, P2 is a subproperty of P1 and S1 has property P2 with value S2 then C1 is a type of S1: (f$p1; dom; $c1); ($p2; sp; $p1); ($s1; p2; $s2)g; f($s1; type; $c1)g) if C1 is the range of P1, P2 is a subproperty of P1 and S1 has property P2 with value S2 then C1 is a type of S2: (f$p1; range; $c1); ($p2; sp; $p1); ($s1; $p2; $s2)g; f($s2; type; $c1)g) sp, sc, dom, range, type are each a subproperty of itself, formally: (;; f(v; sp; v)g); v 2 fsp; sc; dom; range; typeg every property that has a domain or a range is a subproperty of itself, formally: (f($p; v; $y)g; f($p; sp; $p)g); v 2 fdom; rangeg every class that is the domain, the range or a type is a subclass of itself, formally: (f($x; v; $c)g; f($c; sc; $c)g); v 2 fdom; range; typeg 4.2
Constraint satisfaction in RDFS In this section we discuss constraint satisfaction in RDFS. We motivate the need for additional semantic considerations for constraints in RDFS with a simple example.
Example 5. Consider the EGC C = (f(a; sp; $x)g; f($x = b)g) and the following graph:
G = f(a; sp; b); (b; sp; c)g: Observe rst that G j= C. Indeed for every embedding of f(a; sp; $x)g in G we have that $x = b. Under RDFS semantics, however, the constraint should not be satis ed. The reason is that RDFS implies the existence of triples that are not in the graph. In the current example, triple (a; sp; c), for instance, while not part of G, is induced by the semantics of RDFS but does not satisfy the EGC.
Let us call GI the RDF-graph that is de ned (or constructed) from an initial graph G together with all its logical consequences according to the semantics of RDFS as de ned by the S {Constraints in Section 4.1. In this new scenario, we check satis ability of constraints against GI instead of G.
Example 6. Let G be the graph of Example 5. The intentional graph GI is GI = f(a; sp; b)(b; sp; c); (a; sp; c);
(a; sp; a); (b; sp; b); (c; sp; c)g: G j= C, but GI 6j= C as triples (a; sp; a) and (a; sp; c) violate the constraint. We now formalize these notions.
De nition 9 (Intensional Graph). Let G be a graph. The intentional graph of G, denoted as GI , is de ned as the smallest graph with
G GI ;
GI satis es the S {Constraints.
De nition 10. Let C be a constraint. We say that the graph G RDFS-satis es C, denoted as G j=RDF S C i GI j= C.
Theorem 16. Let G be and RDF-graph (without containing S-properties) and C a constraint such that G j= C. Then, G j=RDF S C.
Proof. By de nition G j=RDF S C i GI j= C. But since G contains no RDFS properties G GI . We then have as an immediate consequence that G j=RDF S C. Example 7. Consider the following RDFS-graph:
G = f(a; sp; b)(b; sp; c)g: It is the case that: G 6j=RDFS (f(a; sp; $x)g; f($x = bg)g; G 6j=RDFS (f(a; sp; $x)g; fag ! f$xg); G 6j=RDFS (f(b; sp; $x)g; f(a; sp; $x)g); G 6j=RDFS (f(a; sp; c)g). With the semantics machinery in order, we now turn to the problem of deciding constraint satisfaction in RDFS-graphs.
Lemma 4. Let G be an RDFS-graph. Then GI is computable.
Theorem 17. Let G be and RDFS-graph and SC a nite set of constraints. It is decidable checking whether 8C 2 SC (G j=RDFS C).
We now deal with the use of some of the techniques and results of Section 3 in the context of RDFS-graphs.
11 Lemma 5. Let G be an RDFS-graph and SC a nite set of constraints. It holds that 8C 2 SC, 8C0 2 CS GI j= C [ C0 i G j=RDF S C.
Theorem 18. Let C be a nite set of EGC (resp. TGC, FC or FB) and G an RDFS-graph such that G j=RDF S C. Let C0 be an EGC constraint (resp. TGC, FC or FB). Then it holds that (C [ CS ) ` C0 i G j=RDF S C0.
Proof. Assume (C [ CS ) ` C0. From Lemma 5 and G j=RDF S C, we know that GI j= C [ CS . From Theorem [14] we have, in addition, that G j= C0. As a consequence, we have that G j=RDF S C0. The other direction is trivial. 5
5.1
Related Work
RDF is a W3C recommendation and the reader interested in a thorough
treatment of the language may nd useful the o cial W3C document available at [
Constraints were rst introduced into an RDF framework by Lausen at al. [
Conclusions We have studied constraints in RDFS-graphs in the presence of blank nodes. Included in this paper are decidability results for entailment of di erent types of constraints, sound and complete deductive rules for several combination of constraints, and the analysis of constraint satisfaction in RDFS-graphs. Future lines of research include the development of e cient methods for detecting constraints violation in RDFS-graphs and inconsistency handling.
12
Proof of Theorem 11. The soundness of the rules is quite obvious. Independence: The rules E0-E8 are independent, since they are independent in
dent, since they are independent in Theorem 9 (suppose there are no EGCs in T E ).
We need Rule TE1 to derive f(f(a; a; $x)g; f(b; b; $x)g); (f(b; b; $x)g; f($x = a)g)g ` (f(a; a; x)g; f($x = a)g). We need Rule TE2 to derive f(f(b; b; a)g; f(b; b; b)g); (f(b; b; $x)g; f($x = a)g)g ` (f(b; b; b)g; f($x = b)g). We need Rule TE3 to derive f(f(b; b; a)g; f(a = b)g)g ` (f(b; b; a)g; f(c; c; c)g).
Completeness: Without loss of generality we suppose that all EGCs have a singleton set of equalities and all TGCs have a singleton second set of triples. Let T E = f(Si; f(ti = t0i)g) j 1 i ng [ f(Si; fsig) j n + 1 i qg, T E 6` (S; f(t = t0)g) and T E 6` (S; fs0g). We will construct a graph G that satis es all the constraints of T E but does not satisfy (S; f(t = t0)g) nor (S; fs0g), inducing that (S; f(t = t0)g) nor (S; fs0g) are a logical grounded consequences of T E .
We rst de ne a nite sequence of sets 0; : : : ; p and a nite sequence of functions 0; : : : ; p on VS [ U : 1. 0 = S and 0 is the identity on VS [ U ; 2. 8m; 0 m < p (2.1) 9jm; 1 jm n and 9 hm a homomorphism from Sjm in m (a) with hm(tjm ) 6= hm(t0jm ) and fhm(tjm ); hm(t0jm )g 6 U . If hm(tjm ) 2 V and hm(t0jm ) 2 U interchange tjm and t0jm . De ne m+1 = hm(tjm ) -hm(t0jm )( m) (b) and m+1 = hm(tjm ) -hm(t0jm ) m; or (2.2) 9jm; n + 1 jm q and 9 hm a homomorphism from Sjm in m (a) with hm(sjm ) 62 m. De ne m+1 = m [ fhm(sjm )g (c) and m+1 = m.
m =
hm 1(tjm 1 ) -hm 1(t0jm 1 ) : : : m is a homomorphism from S in We now prove that m p;
n holds that T E ` (S; f(hm(tjm ) = hm(t0jm ))g) p and n + 1 jm
q holds that T E ` (S; fhm(sjm )g) (e).
We actually will prove by downward induction on k: 8m; 0 m p and 8k; 0 k m holds:
14 Since T E ` (Sjm ; f(tjm = t0jm )g), if 1 jm n and T E ` (Sjm ; fsjm g), if n + 1 jm q and hm is a homomorphism from Sjm in m, by (a) we have that T E ` ( m; f(hm(tjm ) = hm(t0jm ))g) (h) if 1 jm n by Rule E6 and T E ` ( m; fhm(sjm )g) (i) if n + 1 jm q by Rule T4.
Hence (f) and (g) hold for k = m.
By downward induction on k, if 1
hp 1(tjp 1 ) -hp 1(t0jp 1 ) : : : hi(tji ) -hi(t0ji ) : : : h0(tj0 ) -h0(t0j0 ). This means that there is a sequence t = 0; : : : ; k; : : : ; m = t0 with for 8k; 0 k < m: 9i; 0 i < p: k = hi(tji ) and k+1 = hi(t0ji ) or k = hi(t0ji ) and k+1 = hi(tji ).
Hence T E ` (S; f( k = k+1)g), for all 0 t0)g), which is a contradiction.
k < m, and hence T E ` (S; f(t = 15 if S0 m then T F B ` (S; S0) (d). if 9i; n + 1 i q 9h; a homomorphism from Si in (e); if 9i; n + 1 i q 9h; a homomorphism from Si in for all S0 with VS0 VS (f).
m then T F B ` (S) m then T F B ` (S; S0), Clearly for m = 0 (d) holds because of Lemma 2, (e) holds because of Rule FB0 and FB1, (f) holds because of (e) and Rule TFB1.
By induction on m (d) holds because of Rules T0-T4, (e) holds because of Rule FB0 and FB1, (f) holds because of (e) and Rule TFB1.
let ( p) = GS.
We have to prove that the graph GS satis es all the constraints of T F B but does not satisfy (S) nor (S; S0): for 8i; 1 i n holds that GS j= (Si; Si0), because of 3. above; for 8i; n + 1 i q holds that GS j= (Si). Indeed, let 9i; n + 1 i q with GS 6j= (Si); then there is an embedding e of Si in GS; 1 e is a homomorphism from Si in p; hence by Rule FB1 T F B ` ( p) and since T F B ` (S; p) we obtain T F B ` (S) by Rule TFB1, which is a contradiction.
GS 6j= (S; S0); let on the contrary GS j= (S; S0), then every embedding of S in GS is also an embedding of S0 in GS; hence every homomorphism from S in p is also a homomorphism from S0 in p and S0 p, but by (d) with m = p, we deduce T F B ` (S; S0), a contradiction; GS 6j= (S), since is an embedding of S in GS.