An assumption-based truth-maintenance system

In this paper we (1) define the concept of a Clause Man-agetnent System (CMS) — a generaizatiou of de Kleer’s ATMS, (2) motivate such systems in terms of efficiency of search and abductive reasoning, and (3) characterize the computation affected by a CMS in terms of the concept of prime implicants.’ 1. A Problem-Solving Architecture Figure 1 illustrates an architecture for a problem solving system consisting of a domain dependent Reasoner cou-pled to a domain independent Clause Management System (CMS). For our present purposes, the Reasoner is a black box which, m the process of doing whatever it does, oc-casionally transmits a propositional clause2 to the CMS. The Reasoner is also permitted to query the CMS any time it feels so inclined. A query takes the form of a proposi-tional clause C. The CMS is expected to respond with every shortest clause S for which the clause S V C is a log-ical consequence, but S is not a logical consequence, of the clauses thus far transmitted to the CMS by the Reasoner. In Section 2 we show why obtaining such S’s is important for many Al systems. For example, for abductive reason-ing-‘S will be an hypothesis, which, if known, sanctions the conclusion C. For efficient search-~Sdefines a most general context in which C holds. A traditional ATMS/TMS is a restricted CMS in which (1) the clauses transmitted to the CMS are limited to be either Horn (i.e., justifications) or negative (i.e., nogoods)