PURPOSE: To provide a proof tree display device which can easily and accurately grasp the proof structure.
CONSTITUTION: When a partial proof tree included in a certain proof tree is designated by a direct or indirect instruction given from a user through an input device 5, a proof display processing part 2 reads the proof tree out of a proof storage part 1 and displays the proof tree on a display means 5 after changing it automatically or in response to the user's instruction. At the same time, the proof tree can be replaced with the partial proof tree by the identifier generated at an identifier processing part 4 or the identifier can be added to the partial proof tree. Furthermore the premise and conclusion part of the proof tree can be reversed to each other and displayed or the conclusion part can be stored in a prescribed length and displayed. Then the sequence of the premise part of the relevant proof tree can be changed by the rule defined at a rule storage part 6 so that the sequence is coincident with the sequence of the premise part set for definition of the rule.
OTANI TAKESHI
OHASHI KYOKO
SAWAMURA HAJIME
