FEATURING GENERATING DEVICE FOR MODEL OF PROPOSITION MODAL LOGIC

摘要

PURPOSE: To automatically generate featuring for a model in a modal logic system from an axiom. ;CONSTITUTION: An axiom for determining a modal logic system is inputted from an input part 1. A prefixed tableau generating part 2 applies a branch modification rule stored in a rule table 3 to respective inputted axioms and generates a set consisting of branches (a list consisting of prefixed code expressions as elements) as elements. The set is called as a prefixed tableau (abbreviated as tab). An one-stage predicate logical expression generating part 4 inputs the tab and generates a first-order predicate logical expression. The expression expresses a minimum relational expression for converting the axiom into a theorem. An output part 5 collects one-stage predicate relational expressions prepared for respective axioms as a list and outputs the list.;COPYRIGHT: (C)1996,JPO