#### Reason Maintenance

There are at least two reasons why it is interesting to incorporate reason maintenance into a system like the one proposed here. The first is, that it may prove valuable not to dispose of the answers found to queries, but to keep them in order to be able to respond faster if the same queries or instances thereof occur again (similar to the use of lemmata in mathematics). As the knowledge base, however, is of dynamic nature, lemmata are only useful if their origins are remembered. The second reason is that we can't be sure that a knowledge base is globally consistent. So it is worthwile looking for nogoods and reporting them, so that the master component is aware of them, or at least it can be guaranteed that in a single `explanation' (proof) no inconsistent material is used (a kind of paraconsistency).

Fehrer [5] shows how a reason maintenance system based on an arbitrary basic logic can be described logically. He also shows there, how an inference system can be obtained, given a calculus (axioms and set of inference rules) for the basic logic. As a special case we can get a system for .

At this stage this result is only of theoretical interest. The main advantage for using terminological logics, instead of full first order logics, lies in the fact that they have efficient algorithms for decidable fragments. The compound logic resulting from putting the reason maintenance onto unfortunately cannot always make use of these algorithms (If we are content with only keeping track of the origins of lemmata generated so far, there is no problem, for the derived calculus inherits all the important properties from its ancestor, so the algorithms can be adapted in a simple manner). This is in essence due to the fact that in order to check for nogoods we have to generate all possible derivations of the falsum. If, however, we start with a possibly inconsistent knowledge base some proof strategies do not yield all possible derivations, for example, strategies incorporating set of support. But, since decidability as well as completeness is preserved in the compound system, it should be possible to devise algorithms with acceptable properties for that task.

At the moment, MOTEL allows the removal of terminological and assertional sentences from the knowledge base. For example, if our knowledge base contains the assertional sentence assert_ind(a,and([C,D])), we are able to remove it using the command delete_ind(a,and([C,D])). But it is not possible to remove a part of the assertional sentence using for example delete_ind(a,C). Intuitively, the later command should result in a knowledge base still containing assert_ind(a,D)).

Next: References Up: The MOTEL Knowledge Representation System Previous: Abductive Reasoning [an error occurred while processing this directive]