Files in this item
|(no description provided)|
|Title:||Reasoning with model-based belief revision semantics: Theory and implementation|
|Author(s):||Chou, Seng-cho Timothy|
|Doctoral Committee Chair(s):||Winslett, Marianne|
|Department / Program:||Computer Science|
|Degree Granting Institution:||University of Illinois at Urbana-Champaign|
|Abstract:||Belief revision semantics appear promising as a definition for the meaning of updates to logical knowledge bases. Numerous model-based belief revision semantics have been proposed in the literature in recent years. It is not at all clear, however, how to translate a proposed model-based semantics into a procedure suitable for implementation. As a result, it becomes hard for one to analyze and identify the practical limits of these revision semantics. In this thesis, we propose an architecture for implementing model-based theory revision semantics, discuss the major algorithms implemented in our prototype system, Immortal, analyze the complexity of the algorithms, and report some results from the implementation of the algorithms. The key feature of our algorithms, as shown in the complexity analysis, is that while belief revision is intractable in general, the expected running time of our algorithms will be polynomial for many interesting cases.
The proposals for these revision semantics to date do not fully support updates involving equality. This thesis extends model-based update semantics to support updates involving equality, by permitting changes in both universe composition and in function interpretations in the models being updated. These theoretical extensions are needed for problems in more complex domains. Adding equality into our prototype system presents some new challenges. In particular, revision problems involving equality will have much larger domains of discourse with more relationships among objects to record and remember. We discuss the necessary extensions in detail.
The contributions of this thesis can be summarized as follows: (1) reduce the theoretical revision semantics into an actual implementation based on a set of algorithms which are proven correct; (2) show that the implementation can be practically used in certain interesting problems and that the implemented heuristics actually work efficiently for certain problems; (3) extend model-based revision semantics to handle equality in terms of changes in function interpretations and universe compositions, making the semantics useful for more complex problems; and (4) equip Immortal with a generic capability for handling equality and changes in the composition of relevant terms of models, an important step towards making the implementation suitable for full-blown first order theories.
|Rights Information:||Copyright 1992 Chou, Seng-cho Timothy|
|Date Available in IDEALS:||2011-05-07|
|Identifier in Online Catalog:||AAI9215793|