Information Technology Reference
In-Depth Information
represented by the node. Finally, the TMS can mark a node as a contradiction, to
represent the inconsistency of any set of beliefs which enter into an argument for
the node. In this case, the TMS invokes the truth maintenance procedure to make
any necessary revisions in the set of beliefs. The TMS locates the set of nodes to
update by finding those nodes whose well-founded arguments depend on
changed nodes. When this happens, another process of the TMS,
dependency-directed backtracking, is also carried out to analyze the well-founded
argument of the contradiction node; then the contradiction can be eliminated
according to locate and delete the assumptions occurring in the argument.
The TMS provides two services: truch maintenance and dependency-directed
backtracking. Both of these services are carried out on the basis of the
representation of reasons for beliefs.
1. Representation of Reasons for Beliefs
A node may have several justifications, each justification representing a
different reason for believing the node. A node is believed if and only if at least
one of its justifications is valid, i.e., at least one of its justifications can be
deduced from the current knowledge base (where these beliefs generated
according to assumptions are also included in this knowledge base).
In the TMS, each proposition or each rule can all be represented as a node.
Each node is of the following two types:
the IN-node which has at least one valid justification, and
the OUT-node which has no valid justifications.
Therefore, there are four states for the knowledge of each proposition p: an
IN-node for p, an OUT-node for p, an IN-node for ¬p, and an OUT-node for ¬p.
Each node has its justifications. The TMS employs two forms for
justifications, called support-list (SL) and conditional-proof (CP) justifications.
The former is used to represent reasons for believing the node, while the later is
used to record the reasons for contradiction.
Each SL justification is of the following form:
( SL (<IN-list>) (<OUT-list>))
(2.21)
A SL justification is valid if and only if each node in its IN-list is IN-node, and
each node in its OUT-list is OUT-node.
For example, consider the following SL justifications:
