Abstract

The challenge we address is how to support non-monotonic reasoning tasks over large-scale knowledge bases of rich expressive form. We identify a central problem of updating: which parts of the previous retractable conclusions are safe, i.e., unaffected, when various new axioms are added? This problem is important not only for the task of belief maintenance and revision, but also for specification and for inference. The difficulty arises because non-monotonicity implies potential globality of conflicting interaction. We attack the problem at a logical level, choosing the circumscription formalism as our vehicle of analysis for its mathematical convenience and expressive power. ;This dissertation provides a primary groundwork for implementing circumscriptive non-monotonic reasoning systems that go beyond previous ones in several respects: to perform forward inference and to maintain a body of valid conclusions, as well as to answer queries, for more expressively complex and larger-scale theories. Our major results build sequentially. We extend the circumscription formalism by generalizing the idea of prioritization so as to enable, for example, the more adequate representation of source reliability and of default inheritance networks. We show that non-monotonic theories are hierarchically decomposable in a manner analogous to programming languages with side effects. We demonstrate several broad cases of safeties of updating, including updating with new default rules. Enabling conditions include syntactic independence and positivity, as well as relative prioritization. We define a generalized "assumption-based" truth maintenance scheme to support inference and belief revision