A Unifying Logical Framework for Reason Maintenance

Abstract

We present a way to describe Reason Maintenance Systems using the same formalism for justification based as well as for assumption based approaches. This formalism uses labelled formulae and thus is a special case of Gabbay’s labelled deductive systems. Since our approach is logic based, we are able to get a semantics oriented description of the systems in question. Instead of restricting ourselves to e.g. propositional Horn formulae, as was done in the past, we admit arbitrary logics. This enables us to characterize systems as a whole, including both the reason maintenance component and the problem solver, nevertheless maintaining a separation between the basic logic and the part that describes the label propagation. The possibility to freely vary the basic logic enables us to not only describe various existing systems, but can help in the design of completely new ones. We also show, that it is possible to implement systems based directly on our labelled logic and plead for “incremental calculi” crafted to attack undecidable logics. Furthermore it is shown that the same approach can be used to handle default reasoning, if the propositional labels are upgraded to first order.