Clause Management Systems (CMS)

In this paper, we study the full extent of the Clause Management System (CMS) proposed by Reiter and de Kleer. The CMS is adapted specifically for aiding a reasoning system (Reasoner) in explanations generation. The Reasoner transmits propositional formulae representing its knowledge to the CMS and in return, the Reasoner can query the CMS for concise explanations w.r.t the CMS knowledge base. We argue that based on the type of tasks the CMS performs, it should represent its knowledge base $\Sigma $ using a set of prime implicates $PI(\Sigma )$. The classification of implicates as prime, minimal, trivial and minimal trivial is carefully examined. Similarly, the notion of a support (or roughly, an explanation) for a clause including prime, minimal, trivial and minimal trivial is also elaborated. The methods to compute these supports from implicates and a preference ordering schema for the set of supports for a given clause are also presented. The generalization of the notion of a minimal support for a conjunction of clauses is also shown. Finally, two logic based diagnostic reasoning paradigms aided by the CMS are shown to exemplify the functionality of the CMS.