An Example of Use of the JTMS
NODE ASSERTION JUSTIF COMMENT
N1 Day (M) = wedn. (SL ( ) (N2)) assumed
N2 Day (M) ° wedn nil not just.ed
R37: If .... then Time(M) = 9.00
N3 Time(M) = 9.00 (SL (37, 43) ( )) just.ed
The PS finds that the room is already busy on Wednesday at 2 p.m. It notifies this contradiction to the JTMS which creates the node
N4 Contrad.-1 (SL (1, 3) ( )) just.ed
Since a contradiction is asserted (made IN), the DDB procedure is invoked. The DDB procedure tries to identify (recursively from the justification of the contradiction) an assumption (or a set of assumptions), whose removal would cause the contradiction t
N5 Nogood -1 (CP 4 (1, 3) ( )) just.ed
which is justified by a 'Conditional Proof' justification, which is valid if the consequent node is always IN whenever the nodes in the in-hypotheses are IN and the nodes in the out-hypotheses are OUT. The CP justification record a logical derivation that