(22) Parallel Model Generation Theorem Prover: MGTP

	Machine:     PIM
	Environment: PIMOS
	Language:    KL1
	Source Code: 2 KB
	Documents:   Manual (Japanese/English)

Overview

MGTP is a massively parallel, high performance theorem prover on finite domain first order priblems.

Parallel theorem prover for the range restricted(every variable in succeedent appears at least once in antecedent) problems.

This theorem prover is designed for a variety of applications which need a powerful inference engine on finite domain.
This system enjoys the excelent performance of PIM by compiling the problem into KL1 clauses.
This is a massively parallel theorem prover that performs linear speed-up with the number of processors.

MGTP consists of a problem compiler and an interpreter.

The return value of MGTP is a set of models if the problem is satisfiable, or an nil list if the problem is unsatisfiable.