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

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