bases (both concept consistency and concept subsumption) to deciding satisfiability of a formula of converse-PDL. Reasoning in converse-PDL is decidable in EXPTIME (Kozen & Tiuryn, 1990), and since the encoding is polynomial (De Giacomo & Lenzerini, 1994a) we obtain an EXPTIME decision procedure for unrestricted concept consistency and concept subsumption in ALUNI knowledge bases.  A simplified form of the encoding, which can be applied to decide unrestricted concept consistency in ALUNI has also been presented by Calvanese et al. (1994).

## 6.2.2 Finite Model Reasoning

We remind that reasoning on a knowledge base with respect to finite models amounts to check either finite concept consistency or finite concept subsumption, for which only the finite models of the knowledge base must be considered.

For finite model reasoning, the techniques based on a reduction to reasoning in PDLs are not applicable. Indeed, the PDL formula corresponding to an ALUNI knowledge base contains constructs both for converse programs (corresponding to inverse roles) and for functionality of direct and inverse programs, and thus is a formula of a variant of PDL
which does not have the finite model property (Vardi, 1985).  However, after encoding functionality, one obtains a converse-PDL formula, and since converse-PDL has the finite model property (Fischer & Ladner, 1979), this formula is satisfiable if and only if it is finitely satisfiable. This shows that the encoding of number restrictions (and in particular the encoding of functionality), while preserving unrestricted satisfiability does not preserve finite satisfiability (De Giacomo & Lenzerini, 1994a).

For finite model reasoning in ALUNI one can adopt a different technique, which is based on the idea of separating the reasoning process in two distinct phases (see Calvanese, 1996c, for full details). The first phase deals with all constructs except number restrictions, and builds an "expanded knowledge base" in which these constructs are embedded implicitly in the concepts and roles. In the second phase the assertions involving number restrictions are used to derive from this expanded knowledge base a system of linear inequalities. The stem is defined in such a way that its solutions of a certain type (acceptable solutions) are directly related to the finite models of the original knowledge base. In particular, from each acceptable solution one can directly deduce the cardinalities of the extensions of all concepts and roles in a possible finite model. The proposed method allows one to establish for ALUNI EXPTIME decidability for finite concept consistency and for special cases of finite concept subsumption. By resorting to a more complicated encoding one can obtain a 2EXPTIME decision procedure for finite concept subsumption in ALUNI in general (Calvanese, 1996a, 1996c).

Reasoning with respect to finite models has also been investigated in the context of dependency theory in databases. As shown by Casanova, Fagin, and Papadimitriou (1984) for the relational model, when functional and inclusion dependencies interact, the dependency implication problem in the finite case differs from the one in the unrestricted case. While the implication problem for arbitrary functional and inclusion dependencies is undecidable (Chandra & Vardi, 1985; Mitchell, 1983), for functional and unary inclusion dependencies it is solvable in polynomial time, both in the finite and the unrestricted case (Cosmadakis et al., 1990).