Information Technology Reference
In-Depth Information
The dependency-directed backtracking mechanism will be uased to recognize the
cause of the contradiction and construct a new default assumption.
3. Dependency-Directed Backtracking
When the TMS makes a contradiction node as IN-node, it will invoke the
dependency -directed backtracking to find and remove at least one of the current
assumptions in order to make the contradiction node as an OUT-node. Let C be
the contradiction node. The dependency -directed backtracking is composed of
the following three steps.
Step 1. Trace through the foundations of the contradiction node C to find the
set S={A
1
…,A
n
} which is composed of maximal assumptions underlying C.
Where A
i
is called a maximal assumption underlying C if and only if A
i
is in C's
foundations and there is no other assumption B in the foundations of C such that
A
i
is in the foundations of B.
Step 2. Create a new node NG to represent the inconsistency of S. NG is
also called as nogood node for representing the following formula:
A
1
∧
…
∧
A
n
false
which is equivalent with
¬(A
1
∧
…
∧
A
n
) (1)
Node NG has the following CP justification:
( CP C S ( ) ) (2)
Step 3. Select some maximal assumption A
i
from S. Let D
1
,…,D
k
be the
OUT-nodes in the OUT-list of A
i
's supporting justification. Select D
j
from this set
and justify it with
( SL (NG A
1
… A
i-1
A
i+1
… A
n
) (D
1
… D
j-1
D
j+1
… D
k
) ) (3)
If the TMS finds other argumrnts so that the contradiction node C is still
IN-node after the addition of the new justification for Dj, repeat this backtracking
procedure.
