Background: assumption based truth maintenance

An ATMS is a mechanism that keeps track of how each piece of inferred information depends on presumed information and facts and of how inconsistencies arise. In an ATMS, each piece of information used or derived by the problem solver is stored as a node. Certain pieces of information are not known to be true and cannot be inferred from other pieces of information, yet plausible inference may be drawn from them. Such nodes are categorised by a special type and referred to as assumptions.

Inferences between pieces of information are maintained within the ATMS as dependencies between the corresponding nodes. In its extended form (see [8]; or [18]), the ATMS can take inferences, called justifications of the form $n_i\wedge\ldots\wedge n_j\wedge\neg n_k\wedge\ldots\wedge\neg n_l\rightarrow n_m$, where $n_i,\ldots,n_j,n_k,\ldots,n_l,n_m$ are nodes that the problem solver is interested in. An ATMS can also take a specific type of justification, called nogood, that leads to an inconsistency, of the form $n_i\wedge\ldots\wedge n_j\wedge\neg n_k\wedge\ldots\wedge\neg n_l\rightarrow\bot$ (meaning that at least one of the statements in $\{n_i,\ldots,n_j,\neg n_k,\ldots,\neg n_l\}$ must be false). In the ATMS, these nogoods are represented as justifications of a special node, called the nogood node.

Based on the given justifications and nogoods, the ATMS computes a label for each (non-assumption) node. A label is a set of environments and an environment is a set of assumptions. In particular, an environment $E$ depicts a possible world where all the assumptions in $E$ are true. Thus, the label ${\cal L}(n)$ of a node $n$ describes all possible worlds in which $n$ can be true. The label computation algorithm of the ATMS guarantees that each label is:

• Sound - All assumptions in any environment within the label of a node being true is a sufficient condition to derive that node:

  $$\forall E\in{\cal L}(n),[(\wedge_{n_i\in E}n_i) \wedge(\wedge_{\neg n_i\in E}\neg n_i)]\vdash n$$

  
  

• Consistent - No environment in the label of a node, other than the nogood node, describes an impossible world:

  $$\forall E\in{\cal L}(n),[(\wedge_{n_i\in E}n_i)\wedge (\wedge_{\neg n_i\in E}\neg n_i)]\nvdash\bot$$

  
  

• Minimal - The label does not contain possible worlds that are less general than one of the other possible worlds it contains (i.e. environments that are supersets of other environments in the label):

  $$\forall E\in{\cal L}(n)\nexists E'\in{\cal L}(n), E'\subset E$$

  
  

• Complete - The label of each node, other than the nogood node, describes all possible worlds in which that node can be inferred:

  $$\begin{split}\forall E,&[(\wedge_{n_i\in E}n_i) \wedge (\wedg... ... \wedge (\wedge_{\neg n_i\in E'}\neg n_i) \vdash n] \end{split}$$