Author:

Abstract:

In the domain of knowledge representation and reasoning, one studies kno wledge: what types of knowledge there are, how often they are used, how they can be expressed in a formal languange, etc. An important goal of k nowledge representation is to develop formal languages (logics) that can be used to express a wide range of problems, to develop automated reaso ning methods for these languages, and to develop efficient implementatio ns of these reasoning methods. ID-logic is a knowledge representation language that extends classical l ogic with inductive definitions. It can express a large variety of pract ical problems in an intuitive way, and has therefore been promoted as a useful knowledge representation language. Model generation is a very general and widely applicable automated reaso ning method. The topic of this dissertation is propositional model gener ation for ID-logic. As such, this work offers an important contribution to the development of automated reasoning methods for ID-logic. The main part of this dissertation is concerned with the propositional f ragment of ID-logic, called PC(ID), and with model generation algorithms for it. We provide two alternative semantical characterizations of PC(I D), both of which yield important insights in the underlying structure o f PC(ID) theories, and both of which therefore contribute to the underst anding of the model generation task for PC(ID). Also, the second charact erization offers a vocabulary-preserving transformation of PC(ID) theori es to propositional logic. We then study practical model generation algorithms for PC(ID). We discu ss a number of possible strategies, provide various propagation rules, a nd present algorithms for these rules. We have also implemented a propos itional model generator for PC(ID). The rest of the dissertation is concerned with ID-logic itself. We discu ss a methodology of knowledge representation in ID-logic and provide som e examples. We also extend ID-logic with aggregate expressions, thereby extending the applicability of model generation for ID-logic. We study p ropositional model generation algorithms for this extension, and have im plemented such algorithms. Finally, we compare ID-logic to a related for malism, namely ASP, and provide a transformation of ID-logic theories to ASP theories.