(14) Development of an MGTP System on KLIC

[Features of the Software]

• This software facilitates programming on MGTP (Model Generation Theorem Prover) which is a bottom-up theorem-proving system running on KLIC.
• Many functions are available through options.

This software contains the following tools:

1. MGTP Translator:
   Translating MG clauses to KL1 clauses
2. MGTP Interpreter:
   An MGTP inference engine which can interpret MG clauses rather than translated KL1 clauses.
3. Helpful Commands:
   Range-restricted Checker, DOM Inserter, MG-clause Counter, MERC-pattern Generator, MG-clauses Redundancy eliminator, and TPTP-to-MGTP Translator
4. Pre-processors for pruning search space:
   FD (Folding Down) Translator and NHM (Non-Horn Magic Set) translator
5. MGTP Tracer:
   Tracing proving process in MGTP
6. An Interactive Programming Environment for KLIC

[Required Environment]

This software is built on KLIC 2.002.

• Sun SparcStation 10 running SunOS 5.3 (Solaris 2.3) with gcc-2.6.3
• Sun SparcStation 10 running SunOS 5.4 (Solaris 2.4) with gcc-2.6.3
• Gateway P5-120 and P5-133 running Linux 1.3.9 (Slackware 2.3.0) with gcc-2.6.3

[File Configuration]

Expanded archives have the following directories:

bin/

Shell scripts to make use of the software

documents/

Users guide for the software

sample/

Sample programs used in the users guide

src/

Source files of the software

[Others]

[FTP]

• README
• Program and Documents in Japanese [84K]