PROCESSING METHOD FOR INCOMPLETE CERTIFICATION OF THEOREM CERTIFICATION ASSISTANCE SYSTEM

摘要

PURPOSE:To relatively easily structure the effective theorem certification assistance system without using an automatic theorem certification system. CONSTITUTION:In a data structure converting process S22, the certification of a natural arithmetic method is converted into a sequence type formal system and an expression wherein the sufficient certification of the incomplete certification given by a user is not obtained is specified in node retrieval processes S31 and S33 and a decision process S32 for deciding whether an inference rule is used or not. Then premise conditions which can be used to certify the expression are found in an environment part take-out process S35 and the expression and premise conditions are shown to the user in a message display process S36, thereby leaving the subsequent planning of proving operation to the user.