Johan de Kleer
This paper presents a new approach for exploiting Truth Maintenance Systems(TMSs) which makes them simpler to use without necessarily incurring a substantial performance penalty. The basic intuition behind this approach is to convey the locality of the knowledge representation of the problem solver to the TMS. The TMS then uses this locality information to control and restrict its inferences. The new TMSs accept arbitrary propositional formulae as input and use general Boolean Constraint Propagation(BCP) t o answer queries about whether a particular literal follows from the formulae. Our TMS exploits the observation that if the set of propositional formulae are converted to their prime implicates, then BCP is both efficient and logically complete. This observation allows the problem solver to influence the degree of completeness of the TMS by controlling how many implicates are constructed. This control is exerted by using the locality in the original task to guide which combinations of formulae should be reduced to their prime implicates. This approach has been implemented and tested both within Assumption-Based Truth Maintenance Systems and Logic-Based Truth Maintenance Systems.