A Process Theory of Non-monotonic Inference

Abstract

Artificial Intelligence needs a formal theory of the executing the process. At no point is theoremhood in the given logic proceiB of non-monotonic reasoning. Ideally, such a theory would defined or used by LPT itself; LPT deals always with finite, decide, for every proposition and state of the process, whether the program should believe the proposition in that state, or remain agnostic. Without non-monotonic inference rules, non-monotonic inferences cannot be explained in the same relational, rule- based fashion as other inferences. But with such rules, theoremhood is often formally undecidable and thus a useless criterion for our purpose. So how could any system be a "non-monotonic logic programming language"? Our method uses the language, inference rules and proofs of non-monotonic logics, but ignores theoremhood. Instead, it defines states of the reasoning process, and focuses on carrent proof as the criterion for belief. It defines "admissible beliefs" and "valid proof" for given states, and we prove in [5] that a belief is currently admissible iff it is currently proven. The primitive non-monotonic condition is "currently unproven". The theory, Logical Process Theory, can accept a range of non-monotonic logics. It was inspired by Doyle's RMS [3] and is similar to his more recent theory in [4]. A model implementation, WATSON, exists and has been used to write a small diagnostic reasoner, which reasons non-monotonically using violation of expectations and an abstraction hierarchy.