CERTIFICATION DEVICE FOR TENSE PROPOSITION LOGIC

摘要

PURPOSE:To attain the expression of a tense modality in a proposition logic by providing a proposition input means which converts a tense proposition logical expression into a standard format, and a transition diagram generation means which removes transition paths that do not satisfy a possible condition and which gather those of strong connection into one. CONSTITUTION:When the tense proposition logical expression is inputted by a proposition input part 1, a standard conversion part 2 converts the tense proposition logical expression to the standard format, and a tense resolution part 4 resolves the converted standard format and converts to a state transition diagram. A removal part 5 removes the transition paths which do not satisfy the possible condition, and a strong concatenated components summarized part 6 gathers those with strong connection among those appearing in the state transition diagram into one, whereby a result display device 8 displays them. When the proposition logical expression can be satisfied, a transition diagram display device 9 outputs the interpretation in the form of the state transition diagram. Thus, the expression of the tense modability is attained in the proposition logic.