Relating the TMS to Autoepistemic Logic

Abstract

Truth maintenance systems have been studied by many authors and have become powerful tools in AI reasoning systems. From the viewpoint of commonsense reasoning, Doyle's TMS seems most interesting, for it allows nonmonotonic justifications. Its semantics, however, has remained unclear. In this paper, we shall give its declarative description in terms of autoepistemic logic, a kind of nonmonotonic logic. That is, we shall exhibit a one-to-one correspondence between states acceptable to the TMS and stable expansions of autoepistemic formulas attached to justifications. Thus, the TMS turns out to be a theorem prover of autoepistemic logic. For the practical interest, our result also suggests the possibility of implementing better TMS algorithms by using the theorem proving method of autoepistemic logic. 1