A Process Theory of Non-monotonic Inference

1. DEFINITION OF LOGICAL PROCESSES

Briefly, Logical Process Theory (LPT) accepts a triple <L,1,l'>, where L and 1 are the object language and inference rule of some suitable logic, and t, the enameration, is a control parameter. The theory then specifies the admi··ible .tate. of an inference process which obeys that logic and makes inferences in the order indicated by t. A state consists simply of the set of inferences made so far, and the set of formulas taken to be believed by the machine

Th.i· reuarch. wa· 1pon1oretl blf th.e Swetli·h. Board of Tech.niclll Development.

executing the process. At no point is theoremhood in the given logic defined or used by LPT itself; LPT deals always with finite, computable states.

LPT requires of L only that it be a denumerable set of formulas; their grammatical structure and semantics is opaque to LPT and hence unrestricted.

The inference rule 1 may be any set of inference .tep1. An inference step is a triple <M,N,c>, where the monotonic antecedent· M are a set of formulas of L; the non-monotonic antecedent· N are a set of formulas of L; and the con·egaent c is a formula of L. We also require some finite bound on the size of M and N for all inferences in 1.

Informally, an inference <M,N,c> may be read: ifllll th.e formal·· in M are cttrrenlllf believed, anti none of th.e formttla· in N are currently believed, th.en c mull be carrentl11 belie11etl. Note that this is stated as a constraint, not as an imperative (not as "if ... then infer c"). The constraint is understood to apply any state of the process after the inference was made. Because it is a conditional constraint, it does not necessarily force belief in c; for the same reason, it can be safely made at any time, whether its antecedent conditions are satisfied at that time or not.

No further restrictions are placed on L or 1 by LPT. Normally L would be defined by a grammar, and 1 by a set of schemas or rules. The rules of default logic [10[, for example, have the form:

a]b

c

where a, b and c are single formulas; this may be expressed in LPT by the schema <{a},{not b},c>.

We prefer the alternative of introducing non-monotonicity directly into the language L by a modal operator, as in [9[. WATSON uses an operator UNPROVEN. In this case it is convenient to represent the standard first-order inference rules as inferences in which N is always empty, and to obtain all non-monotonicity via one inference schema for introducing the modal operator, <{},{a},"(UNPROVEN a) · >. This may be read "if a is not currently believed, then "(UNPROVEN a)" must be currently believed".

Since L is denumerable and the sizes of M and N have a constant bound, I is also denumerable. We denote enumerations of I by the control parameter t . Intuitively, t represents the order in which individual inference steps are taken by a Logical Process. To take an inference step simply means to add it to the database; the current database in the j:th state is therefore just the set of the first j inferences of t.

To represent sets of beliefs, we defwe an IN/OUT labelling as a total function from L to the set of labels {IN,OUT}. A .tate of the machine is then a pairs = <D,G> of a database D and an IN/OUT labelling G.

An individual inference d = <M,N,c> is 11alid under an IN/OUT labelling G if every formula in M is labelled IN by G, and every formula in N is labelled OUT by G; d is in11alid under G otherwise. Where it is clear which labelling or state is intended, we say simply that d is valid.

A state <D,G> is relazed if for each dED, either the consequent of d is labelled IN by G, or dis invalid under G.

A relaxed state satisfies all the constraints in the database locally, but to eliminate circular proofs, a non-local ordr.,ring must also be imposed. Therefore: a state <D,G> is toell-foanded iff there exists a partial order -< over Lui such that

1. For every formula s labelled IN by G, there is a lED which is valid under G, has s as its consequent, and d-<s, and
2. For every valid dED, for every formula s in the monotonic antecedents M of tl, s-<tl.

Finally, an admi11ible state is one which is both relaxed and well-founded, and its labelling is said to be an admissible labelling for its database.

Having defined the admissible states, the main task at hand is to relate them to proofs. A proof of a formala c is a tree of inferences with c at the root, in which each node has for each of its monotonic antecedents a daughter node proving that antecedent, and has no other d~.ughter nodes. A proof is 11alid in a rtate <D,G> if every inference in the proof tree is contained in D and is valid under G.

(Premises are introduced by inferences with empty M and N. Such inferences are always valid, and may appear at any point in the enumeration. This allows inference and input of new external information to be arbitrarily interleaved.)

2. PROPERTIES OF LOGICAL PROCESSES

The main theorem about Logical Processes correlates belief with current proof: for anu admissible .tate 1 and anu formula c of L, there is a valid proof of c in ·, iff c i1 labelled IN in s. (Proof to appear in [ 5]) .

Some additional properties are as follows (proofs again in [5]):

Admissible states are physically representable: any database is finite, and in any admissible state, the number of formulas labelled IN is finite.

Non-monotonic belief behavior is actually obtained: a formula may be IN in one state and OUT in a later state. This may result either (1) because of new premises being given, or (2) merely due to further inference based on information already available, or any combination of the two.

We call both cases ·non -monotonic inference·, because the set of currently admissible beliefs may vary non-monotonically as the process continues. From the perspective of a process theory of inference, there is no very natural distinction between them, nor much reason to try to find one.

(We have several times met the objection that ·non-monotonicity· has a standard definition, according to which the case 1 above is ·non-monotonicity" and case 2 is something else. Now, ·non-monotonic logic" has indeed a precise and weD-established meaning: any logic in which adding premises may delete theorems. But neither case 1 nor case 2 mentioned theorems; they described non-monotonic inference, as a process in which current proof of a formula may come and go. This is a reasonable use of the term ·non-monotonic inference·, consistent with its common informal use in AI. Certainly, non-monotonicity of beliefs during the inference process is a different matter than non-monotonicity of theorems under addition of premises. The former is computable where the latter is not, and the former explains case 2 where the latter does not allow the question to be put. For Artificial Intelligence, those are advantages. Note also that the set of inference rules which are "non-monotonic" is the same in either sense.)

In a non-monotonic LP, a given database may have zero, one or many admissible labellings. Moreover, its predecessor or successor may independently have zero, one or many admissible labellings. It is therefore possible that an admissible state s may be "inaccessible" under a given t, in the sense that the process cannot reach s while passing on ly through admissible states. However, there is always a permutation of the initial subsequence of t up to and including s, such that every state up to s is admissible.

By a proof adapted from [1], for a database to have zero admissible labellings, it must contain a configuration called an "odd loop", which is usually a kind of "Liar's Paradox" arfllment . By ruling this case out , we guarantee continuity of the sequence of admissible states, and also make possible an efficient reason maintenance algorithm for finding them.

Since the formulas of L are opaque to LPT, LPT cannot say anything about their consistency, in either a model theoretic sense, or in terms of provability of a contradiction. This is only to be expected, however, of a process theory of non-monotonic reasoning, since the purpose of non-monotonicity is to allow a reasoning agent to make unsound but reasonable inferences and then back out of them if they turn out to be inconsistent due to new information or - again, we stress the focus on process - simply due to further reasoning. The only guarantee given by LPT, that of admissibility, is that the system knows exactly what it does and does not have current proof of.

3. WATSON: A MODEL IMPLEMENTATION

WATSON is a model implementation in LISP of a non-monotonic Logical Process. It is a pure forward chaining system. The inference rules are "wired in" to the interpreter, which does nothing but add dependencies (inferences permitted by the rules) to the database. All valid inferences are drawn. Unlike previous systems [2,7] there is no way to "escape to lisp" and manipulate dependencies.

How much can be done with pure non-monotonic inference alone? DIAGNOSE is a small diagnostic reasoner written in WATSON, which uses non-monotonicity both to reason by violation of expectations, and to work downwards in an abstraction hierarchy. So the system is not trivial.

Some inference rules which we cannot state in the format allowed by LPT include a forward chaining analog of negation by failure; conditional proof as in [3] and thus dependency directed backtracking as well; and inferring the set of all currently proven instances of a formula (contrast circumscription [8]) . We have already extended WATSON to use these rules, as well as to allow expression of control in the language: "reasoned control of reasoning" . Revision of LPT to account for these extensions is in progress.