where Ei is a set of ground hypotheses from Gamma on which Ai depends, and the 
function cc is defined as: 



P.72 Function 1


Each time MGTP-1 derives a new ground atom, the consistency of the com-
bined hypotheses is checked by MGTP-2 (see Figure 2). The parallelism comes 
from calling multiple MGTP-2s at once. 



P.72 Figure 2

Figure 2: MTGP+MTGP


Skip Method 

When a clause in Sigma contains the negative occurrences of abducibles H1,...,Hm
(HiinGamma, mgequal0)and is in the form: 



P.72 Function 4


we translate it into the following MGTP rule: 



P.72 Function 5



In this translation, each hypothesis in the premise part is skipped instead 
of being resolved, and is moved to the right-hand side. A model candidate 
containing both H and notequalKH is rejected by the schema: 



P.72 Function 6



This method utilizes the extension and rejection of model candidates supplied 
by the MGTP. An OR-parallelism can be obtained in the way that multiple 
model candidates are kept in distributed memories. In order to avoid possible 
combinatorial explosion in constructing model candidates for the skip method, 
we also showed a way to "cut" model candidates that cannot contribute to 
providing solutions. 


					- 72 -