MGTP System with An Advanced Inference Engine
and
Application Tools

Prof. Makoto Amamiya at Kyushu University

[Features of the Software]

This distribution package provides a high-performance reasoning system based on model-generation theorem prover MGTP, and its applications. The configuration of files in the distribution is as follows:

MGTP System:

Translator
compiles a set of input formulas, called an MGTP program, into a KL1 program.
The translator allows specifying KL1 code within MGTP programs.
High Performance Inference Engine
finds solutions for the input formulas.
The inference engine incorporates the dynamic lemma generation technique, which increases the inferential power dramatically.

MGTP Application Programming Tools:

LR Parser Generator
translates CFG rules into an MGTP program for generalized LR parsing.

[Required Environment]

Since the MGTP system is written in KL1, the system requires the KL1-to-C compiler: KLIC compiler (newer than version 2.0). The KLIC compiler is portable to most UNIX systems, and the MGTP system runs on the same systems as KLIC. For example, the MGTP system is available on Sun Sparc, DEC Alpha, and Linux on an IBM-PC.

[File Configuration]

Expanded directory contains the following directories and files:

COPYRIGHT.j INSTALL.j MANIFEST Overview.j README README.j
documents (Directory for Documents)

ifs-src.eps manual.tex
pim (Directory for Source File on PIMOS)

MGTPst.kl1 (Standard Inference Engine)
DLGst.kl1 (Inference Engine for Dynamic Lemma Generation)
src (Directory for Source File)

Makefile
mgtp.kl1 (Standard Inference Engine)
cmgtp.kl1 (Inference Engine for CMGTP)
dlg-mgtp.kl1 (Inference Engine for Dynamic Lemma Generation)
mg2kl1.kl1 (MGTP to KL1 Translator with KL1 interface)
mgtp (MGTP compiler)
cfg2mg (CFG-to-MGTP program Translator)
unify.kl1 fm.kl1 cfg2y.kl1 y2mg
samples (Directory for Test Data)

G0.cfg G1.cfg (Simple Grammars)
G0.s G1.s (Input Scentences)
hase2.mg hase6.mg (MGTP program samples)

[FTP]

README
Program and Documents in Japanese [40K]