Using similar transformations, a close relationship to the problem of query containment studied in the database field has been shown: checking query containment for non recursive conjunctive queries is equivalent to checking projection between SGs (Chein et al., 1998; Mugnier, 2000).

## 23  The Deduction Problem: Computational Complexity

For the sake of brevity, we consider in what follows that SGs are given in normal form, and put into normal form if needed after a modification. And, since a SG does not need to be a connected graph, we conflate a set of SGs with the SG obtained by performing the disjoint union of its elements. In the following definition, for instance, the SG G represents a set of SGs Definition 4 ( SG-DEDUCTION ) Let G and Q be two SGs defined on a support S. Q can be deduced from G if Q ≥ G .

Chein and Mugnier (1992) have shown that projection checking is NP-complete with a reduction from CLIQUE. Equivalence with CSP (satisfiability of a constraint network) was also used later (Feder & Vardi, 1993; Mugnier & Chein, 1996), and independently in a very similar model by Rudolf (1998) (see part 8 of this paper). We give below another proof of this result based on a reduction from 3-SAT. Though more complicated than the previous ones, this reduction is the basis for other reductions presented later in this paper.

The following theorem keeps into account the complexity of concept and relation type checking, though in this paper this test can obviously be performed in polynomial time since concept and relation types are only labels partially ordered in a hierarchy.

Theorem 2 (Chein & Mugnier, 1992) SG-DEDUCTION is a NP-complete problem, iff type checking in S  belongs to NP.

Proof: First see that if type checking is in NP, then SG-DEDUCTION is also in NP: a projection, enriched by certificates for all type checks used, is a polynomial certificate.  The reciprocal is obviously true. We now show that, even if type checking can be done in Θ(1),
SG-DEDUCTION is NP-complete.

Let us now build a reduction from 3-SAT. The input of 3-SAT is a formula F in 3conjunctive normal form (3-CNF), i.e. a conjunction of disjunctions (clauses), each with at most three literals, and the question is whether there is a truth assignment of the variables of F such that F is true. Notice the classical 3-SAT problem considers clauses with exactly three literals, but for further proofs we prefer to use the above variant.

Let F = C 1 A . . . A C k be an instance of 3-SAT. W.l.o.g. we suppose that ea variable appears at most once in a clause. Let us create four concept types for each variable x : x, xf, xt and xv . We also create one relation type C i for each clause C i , and a relation type val . Each concept type xv is greater than xt and xf , these are the only possible comparisons between distinct types.

We build the graph G( F ) as follows: for every variable x in F , we have three concept nodes [x], [xt] and [xf] in G(F) and two relation nodes typed val linking the first to the latter ones (intuitively, it means that the variable x can be valuated by true or false ). Let