Unrestricted and Finite Model Reasoning in Class-Based Representation Formalisms

Diego Calvanese

1996. Number VIII-96-2 of Collana delle tesi del Dottorato di Ricerca in Informatica.

In this thesis we devise in an incremental manner a set of abstract knowledge representation languages, called L-languages, and study reasoning on them. Using L-languages one can build complex class and attribute expressions and use these to define schemata for the representation of knowledge at the intensional level. We first show that L-languages subsume in their more expressive variants the structural aspects of most of the representation formalisms used both in Knowledge Representation and in Databases. The main part of the thesis is concerned with the design of effective techniques for intensional reasoning on L-schemata and the study of their computational properties. We first characterize the intrinsic complexity of reasoning on L-schemata for a relevant class of languages and different types of schemata. The expressivity of L-languages causes the finite model property not to hold and we analyze separately reasoning with respect to both finite and unrestricted models. In the case of unrestricted models we extend the correspondence between L-languages and Propositional Dynamic Logics (PDLs) and show decidability in deterministic exponential time for reasoning in several L-languages. In the case of finite models we devise a novel reasoning method which exploits linear programming techniques. The resulting algorithms works in worst case deterministic single and double exponential time, and exhibit efficient behaviour in meaningful practical cases.

   title = "Unrestricted and Finite Model Reasoning in Class-Based
Representation Formalisms",
   year = "1996",
   author = "Diego Calvanese",
   school = "Dipartimento di Informatica e Sistemistica, Università di
Roma "La Sapienza"",
   note = "Number VIII-96-2 of Collana delle tesi del Dottorato di Ricerca in
ps.gz pdf