Nonmonotonic Reasoning as a Temporal Activity

TL;DR

This paper introduces a dynamic reasoning system (DRS) that models reasoning as a temporal activity, allowing for nonmonotonic belief revision and application-specific controllers, demonstrated through classic reasoning puzzles.

Contribution

It formalizes a framework for dynamic, temporal reasoning systems with algorithms for nonmonotonic belief revision, applicable to first-order logic and reasoning puzzles.

Findings

Demonstrates resolving classic nonmonotonic puzzles within DRS

Provides a formal, computable foundation for temporal reasoning systems

Shows how controllers guide reasoning in response to inputs

Abstract

A {\it dynamic reasoning system} (DRS) is an adaptation of a conventional formal logical system that explicitly portrays reasoning as a temporal activity, with each extralogical input to the system and each inference rule application being viewed as occurring at a distinct time step. Every DRS incorporates some well-defined logic together with a controller that serves to guide the reasoning process in response to user inputs. Logics are generic, whereas controllers are application-specific. Every controller does, nonetheless, provide an algorithm for nonmonotonic belief revision. The general notion of a DRS comprises a framework within which one can formulate the logic and algorithms for a given application and prove that the algorithms are correct, i.e., that they serve to (i) derive all salient information and (ii) preserve the consistency of the belief set. This paper illustrates the idea with ordinary first-order predicate calculus, suitably modified for the present purpose, and an example. The example revisits some classic nonmonotonic reasoning puzzles (Opus the Penguin, Nixon Diamond) and shows how these can be resolved in the context of a DRS, using an expanded version of first-order logic that incorporates typed predicate symbols. All concepts are rigorously defined and effectively computable, thereby providing the foundation for a future software implementation.