The ATMS does not take part in any problem solving. It is required to indicate what can be believed in the current environment i.e. under a given set of assumptions so whenever the problem solver draws a conclusion, it passes that conclusion as well as the justification to the ATMS. The ATMS then incorporates the new information into its set of beliefs and indicates if any contradictions have arisen.

Figure 1. ATMS Architecture

The input to an ATMS consists of a sequence of propositional horn clauses presented over a period of time. Figure 1 shows three logical expressions used to make an inference. When these are transmitted to the ATMS, each expression is converted to an atom because the ATMS does not care about the inference itself hence all of the clauses that the ATMS sees are propositional. A further example of input to the ATMS is the sequence of clauses:

assume a. p :- a, b. assume b. p :- b, c, d. assume c. assume d. q :- a, c. assume e. q :- d, e. :- a, b, e. r :- p, q.

In
this case, we have entered all of the assumptions first, followed by a
*nogood*. A nogood set is a set of propositions that cannot be true
simultaneously, so *a*, *b*, and *e* cannot all be true at
the same time. The rest of the horn clauses indicate conclusions drawn by the
problem solver. For example, it was concluded that *p* was true because
a and *b* where assumed to be true and *r* was found to be true
because *p* and *q* are hypotheses supported by the current set
of assumptions.

Whenever assumptions are made and each time a clause is entered, we update a graph in which each node represents a belief. The information above would result in the graph shown in Figure 2, drawn as and "and-or" tree where the arcs indicate those propositions that are to conjoined.

Figure 2: ATMS graph

The information stored in each node is:

- The node description (e.g. a, b, c,
*etc*.) - Consequents of the node (the parent nodes in the graph)
- Justifications for the node (the child nodes, grouped by the clause of origin)
- The node's label (indicating the assumptions upon which this belief is based)

The label is a set of *environments* and an environment is a set of
assumptions under which the node is believed true. For example we can describe
each of the nodes in the graph using Prolog notation as follows:

node(p, [r], [(p :- a, b), (p :- b, c, d)], {{a, b}, {b, c, d}}). node(q, [r], [(q :- a, c), (q :- d, e)], {{a, c}, {d, e}}). node(r, [], [(r :- p, q)], {{a, b, c}, {b, c, d, e}}).

Thus,
*r*, can be believed if we assume that *a*, *b* and
*c* are true at the same time or *b*, *c*, *d* and
*e* are all true. Note that the assumptions for *r* are obtained
by propagating the assumptions from its descendants. The reason for keeping the
label is so that we can easily determine whether a proposition is believable or
not.

*P*, *q* and *r* are nodes that have been derived by some
deduction on the part of the problem solver. There are three types of nodes
that are not derived. They are:

- Assumptions:
- these nodes are that are justified by themselves e.g.

node(a, [], [], {{a}}).

- Premises:
- these are nodes representing facts that do not need justification, e.g.

node(g, [], [], {{}}).

- Note that the label contains an empty environment meaning that the proposition can be believed without having to assume anything.
- False:
- false is the node implied by all nogood sets:

node(false, [], [], {}).

If, after updating the graph, a node has an empty label then it is not believed to be true any more. This is because there is no set of assumptions that can justify the conclusion. An empty label results when a set of assumptions (i.e. an environment) contains a nogood set and therefore must be removed since the assumptions are contradictory. If all of the environments are removed, the label becomes empty indicating that the proposition cannot be believed. For example, r could have been derived by the following rules:

p :- a, b. q :- d, e. _________ r :- p, q.

However,
this would require r to depend on the assumptions {a, b, d, e} which would
appear as an environment in *r*'s label. Since this contains a nogood
set, this environment must be removed from the label.

In addition to removing nogood environments, the ATMS algorithm also ensures
that a label does not contain environments that are supersets of others since
the label would then have redundant information. For example, *r*'s
label could contain two environments {a, b, c} and {a, b, c, d}. Since {a, b,
c} subsumes {a, b, c, d}, the second environment is redundant and can be
removed.

We refer the reader to de Kleer for a detailed description of the ATMS update
algorithm. For our purposes, the main operations of the ATMS are best seen in
an example. Suppose that the ATMS has been given all but the final horn clause
`r:- p, q`. When this clause is presented, it is up to the
ATMS to adjust its beliefs. This proceeds as follows:

- Find the labels for the antecedents in the clause

p: {{a, b}, {b, c, d}}

q: {{a, c}, {d, e}} - Find all combinations of assumptions for
*p and q*.

{{a, b, c}, {a, b, d, e}, {a, b, c, d}, {b, c, d, e}} - Eliminate all environments that are no good (i.e. are supersets of the
nogoods).

{{a, b, c}, {a, b, c, d}, {b, c, d, e}} - Eliminate all environments that are supersets of others in the label.

{{a, b, c}, {b, c, d, e}} - The new label is now attached to the node
*r*. If*r*had already existed and had its own consequents then*r'*s label would have to be propagated recursively through to the consequents.

From this example, it can be seen that the ATMS algorithm requires frequent set union operations to calculate a new label and also many subset tests to find nogoods and environments that are subsumed by other environments.

de Kleer, J. (1986). Extending the ATMS, *Artificial Intelligence*,
**28**(1).

de Kleer, J. (1986). Problem Solving with ATMS, *Artificial Intelligence*,
**28**(1).

CRICOS Provider Code No. 00098G