Syntax and Semantics of a Monotonic Framework for Non-Monotonic Reasoning

We present the proof theory and the model theory of a monotonic framework for default reasoning, and we extend logic programming techniques to this framework. Standard formalizations of default reasoning do not syntactically separate between hard knowledge and conjectural knowledge. Such a separation is fundamental in our framework. To illustrate our approach, we show how it solves the Yale Shooting problem. 1 Introduction To make this paper somewhat conceptually self-contained, we first recall very briefly some general notions on logic programming with ions. We then explain how we apply these ideas to non-monotonic reasoning. Ions have been introduced in [3] for expressing generalized SLD-derivations in a framework where more than one logic program is relevant to the derivation. Essentially, an ion is a pair of the form (Q; g), i.e. a formula g that is given in some logical context Q where it is to be solved. In such a pair, the Q-part "qualifies" (or "puts in context") the g-part. ..