## Finite Model Reasoning in Description Logics

**Diego Calvanese**
*Proc. of the 5th Int. Conf. on Principles of Knowledge
Representation and Reasoning (KR 1996).* 1996.

Both in Knowledge Representation and in Databases representation
formalisms have been developed which offer powerful structuring
capabilities and procedures to reason on a specification. However,
while in Databases the common assumption is that the modeled domain
is finite, this has seldom been an issue in Description Logics. For
the simpler logics, reasoning with respect to finite models amounts
to reasoning with respect to arbitrary ones, but finiteness of the
domain needs to be considered if expressivity is increased and the
finite model property fails. Procedures for reasoning with respect
to arbitrary models in very expressive Description Logics have been
developed, but these are not directly applicable in the finite
case. We show that we can nevertheless capture a restricted form of
finiteness and represent finite modeling structures such as lists
and trees, while still reasoning with respect to arbitrary models.
The assumption of finiteness of the domain is essential, however,
to capture several data models used in Databases. Finite model
reasoning is not so well investigated and decidability is open for
many important cases. The main result of this paper is a procedure
to reason with respect to finite models in an expressive
Description Logic equipped with inverse roles, cardinality
constraints, and in which arbitrary inclusions between concepts can
be specified without any restriction. This provides the necessary
expressivity to go beyond most semantic and object-oriented
Database models, and capture several useful extensions.

@inproceedings{KR-1996,
title = "Finite Model Reasoning in Description Logics",
year = "1996",
author = "Diego Calvanese",
booktitle = "Proc. of the 5th Int. Conf. on Principles of Knowledge
Representation and Reasoning (KR 1996)",
pages = "292--303",
publisher = "Morgan Kaufmann",
}

ps.gz pdf