ABSTRACT 

The goal of our research is to build a parallel automated reasoning system 
on a parallel inference machine(PIM/m), using KL1 and PIMOS technologies. 
The MGTP prover, currently being developed, adopts the model generation 
method. In the development of MGTP, we aim to achieve the following: 

Combine logic programming and automated reasoning, and develop paral-
lelization techniques to implement an efficient first-order theorem prover. 
Offer an advanced inference engine that can be applied to fields such 
as intelligent database systems, hypothetical reasoning, natural language 
processing, and automated programming. 


KEY FEATURES 

Development of clause compiling techniques and meta-programming util-
ities to implement an efficient prover in KL1. 
Development of AND/OR parallelization techniques, thereby achieving 
high scalability and linear speed up on PIM/m(256PEs). 
Development of a support environment to make it easy to use and develop 
MGTP. 
Development of MGTP applications (specification description, abductive 
reasoning, and automated programming). 





MGTP Relative to FGCS


					- 63 -