|
AITEC Contract Research Projects in FY1996 : Software
|
(11) Development of an MGTP System on KLIC
Dr. Ryuzo Hasegawa, Professor, Kyushu University
MGTP :
A Theorem Prover based on Model Generation
by
Ryuzo Hasegawa (Kyushu University)
[Software Features]
- This software facilitates programming on MGTP(Model Generation
Theorem Prover) which is a bottom-up theorem proving system running on
KLIC.
- Many kinds of functions are available through options.
This software includes the following UNIX commands:
- MGTP Kernels:
MGTP(interpreter version), MGTP with folding-up facility,
Constraint MGTP(interpreter version),
MGTP with term-rewriting facility
- MGTP Preprocessors:
Range-restricted Checker, DOM Inserter, MG-clause Counter,
MERC-pattern Generator, MGTP clause compiler,
NHM translator, MG-clauses Redundancy eliminator, and
TPTP-to-MGTP Translator
- GUI
[Required Environment]
This software is built on KLIC 2.002.
Tcl/TK is required when you use GUI system.
We checked that this software can run on:
- 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
- Cray SuperServer 6400 running CRS-OS 5.4 with gcc-2.6.3
[File Configuration]
Expanded archives have the following directories:
- documents/
- Users guide for the software
- mg/
- MGTP sample programs
- klic/
- Source files of the software
- sh/
- Shell scripts to make use of the software
- tcl/
- Shell scripts to make use of the software
[Others]
This software is still under development.
[FTP]
- README
- Program and Documents in Japanese [151.2K]
www-admin@icot.or.jp