

![0_image_0.png](0_image_0.png)

![0_image_1.png](0_image_1.png)

obtained from variables in X 2 (concept nodes typed x or xv and relation nodes typed val) are colored by 1 (i.e. belong to the obligation). Once again, having clauses of bounded size leads to a polynomial transformation. The simple graph G and the positive constraint C
presented in Fig. 12 are obtained from the 3-SAT formula ( a V b V ¬c) ∧ (¬a V c V ¬d ) and the partition X 1 = { a, b}, X 2 = { c, d}
Ea truth assignment of the variables of E s.t. E is true naturally gives a projection from C into G , and reciprocally (as indicated in the proof of Th. 2). Furthermore, any truth assignment for the variables of X 1 naturally gives a projection from C (0) into G 1 and reciprocally. Thus, the question "is it true that for any truth assignment for the variables in X 1 there exists a truth assignment for the variables in X 2 s.t. E is true?" is equivalent to the question "is it true that for any projection π 0 from C [0] into G there exists a projection from C into G extending πο?".

Note that this reduction is less straightforward than the one we proposed in (Baget &
Mugnier, 2001), but it will be used as a basis for the proof of Th. 12. Corollary 2  Deduction in SGC is Π p -complete

## 6. Rules And Constraints: Sec/Src/Srec

In presence of constraints, the two kinds of rules, inference rules R and evolution rules E ,
define two alternative models.

## 6.1 Definitions And Notations

In SEC, G is seen as the initial world, root of a potentially infinite tree of possible worlds, and E describes the possible evolutions from one world to others. The deduction problem asks whether there is a path of consistent worlds from G to a world satisfying Q
DEFINITION 12 ( SEC-DEDUCTION ) Let K = ( G, E,C) be a KB, and let Q be a SG. Q can be deduced from K if there is an E-derivation G = G 0 , . . , G k such that, for 0 ≤ i ≤ k, (G i , C)
is consistent and Q can be deduced from G k In SRC, G provided with R is a finite description of a potentially infinite world, that has to be consistent. Applying a rule to G can create inconsistency, but a further application of a rule may restore consistency. Let us formalize this notion of consistency restoration.