Machine: UNIX/PC Environment: UNIX/MS-DOS Language: Prolog Source Code: 60KB Documents: User's Manual(English,Japanese)
Where an antecedent is a conjunction of A1, A2, ..., An. When n = 0, it gives the initial model(a set of facts). When m = 0, it represents a condition of contradiction. In MGTP, proving starts with the initial model and proceeds from the antecedent to the consequence in a forward reasoning manner.
The range-restrictedness condition is not imposed on problem clauses of MGTP/N. A clause is said to be range-restricted if every variable in the clause has at least one occurrence in its antecedent. This leads to the necessity of unification with an occurs check because atoms appearing in the proof may contain variables. The unification program is written in Prolog for making the unification sound. With Horn clause, it is not necessary to consider case-splitting. Generated atoms are maniplated using the (Prolog) assert function.
In spite of dealing only with Horn clauses, MGTP/N not only solves many mathematical problems such as that of condensed detachment but also is used as a practical tool for mode analyzing in the KL1 compiler.
