Finite Model Reasoning in Description Logics

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",
}