A LOGICAL CHARACTERIZATION FOR TRUTH MAINTENANCE SYSTEMS WITH DEPENDENCY-DIRECTED BACKTRACKING

In this paper we present various logical characterizations of justification-based (nonmonotonic) truth maintenance systems (JTMS). These characterizations, which are proved to be equivalent, aim at describing dependency-directed backtracking (DDB) (i.e., the process of resolving conflicts which can arise when nogoods are allowed in the set of justifications), mainly relying on the intuitive idea that a contrapositrve use of justifications is needed to resolve inconsistencies. The idea is first formalized by means of the notion of three-valued labeling and then through a transformation which explicitly adds all contrapositives of the justifications. An abductive characterization of the JTMS is provided through a further transformation which converts a set of nonmonotonic justifications to a corresponding abduction framework. This approach provides a unifying framework, based on the notion of abduction, for describing both JTMSs and assumption-based TMSs (ATMSs).