Machine: PIM Environment: PIMOS Language: KL1 Source Code: 50 KB Documents: User's Manual ( English / Japanese )
With model sharing, each PE has a copy of the model candidates. An advantage of model sharing is that we can minimize inter-PE communication since most time-consuming subsumption tests and conjunctive matchings can be performed independently at each PE.
With model copying, the model candidates are distributed to each PE. This method can obtain memory scalability and more parallelism than the model sharing method. However, it has the drawback that the communication cost increases since generated atoms need to flow to all PEs for subsumption tests and conjunctive matchings.
where an antecedent is a conjunction of 
, 
, ..., 
. The consequent has at most
one atom. Empty consequent represents a condition of contradiction.
When n = 0 , it gives the initial model ( a set of facts ). In
MGTP, proving starts with the initial model and proceeds from the
antecedent to the consequence in a forward reasoning manner.
The system has a procedural interface for KL1 programs. Two options are available for proving strategy: sorting generated atoms by their weight and deleting useless atoms by their argument pattern.
In spite of dealing only with Horn clauses, MGTP/N solves many mathematical problems such as that of condensed detachment.
