Model Generation Theorem Prover, MGTP 

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: 

1. Combine logic programming and automated reasoning, and develop paral-
   lelization techniques to implement an efficient first-order theorem prover. 
2. 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 -

Parallelization of MGTP 

There are several resources for parallelization of MGTP: 
¥ case splitting 
¥ conjunctive matching in the antecedent part 
¥ subsumption test 

We focused on OR parallelization in case splitting and on AND parallelization 
in conjunctive matching and subsumption test. 

OR Parallelization 

For non-Horn and ground problems, it is sufficient to exploit OR paral-
lelization induced by case splitting. We implemented an OR parallel version 
of MGTP based on the MERC method.

The processor allocation methods we have adopted achieve `bounded-OR' 
parallelization in the sense that OR parallel forking in the proving process is 
suppressed so as to meet restricted resource circumstances. To do this, we 
adopted a scheme, called level restricted allocation. 

We expanded model candidates, starting with an empty model, using a sin-
gle master processor until the number of candidates exceeded the number of 
available processors. We, then, distributed the remaining tasks to slave pro-
cessors. Each slave processor explored the branches assigned without further 
distributing tasks to any other processors. 

This allocation scheme for task distribution works fairly well, since the 
communication cost can be minimized. 




Level restricted allocation

- 67 -

AND Parallelization 

AND parallelization for Horn problems is achieved by exploiting paral-
lelisms inherent in conjunctive matchings and subsumption tests. We im-
plemented an AND parallel version of MGTP based on lazy model genera-
tion. The system adopts the following schemas: the proof unchanging schema 
according to the number of PEs, the model sharing schema (copying in a 
distributed memory architecture), and the master-slave schema. 

Proof Unchanging: Our policy in developing parallel theorem provers is 
   to distinguish between the speedup effect caused by parallelization and 
   the search-pruning effect caused by strategies. A proof-changing prover 
   may achieve super-linear speedup whereas it may cause the strategy to 
   be changed. On the other hand, a proof-unchanging prover allows us to 
   obtain greater speedup as the number of PEs increases, without changing 
   the strategy. 

Model Sharing: The merit of model sharing is that time-consuming sub-
   sumption testing and conjunctive matching can be performed at each PE 
   independently, with minimal inter-PE communication. 

Master-Slave: The master-slave configuration makes it easy to build a par-
   allel theorem prover by simply connecting a sequential version of MGTP 
   on a slave PE to the master PE. Since slave processes spontaneously ob-
   tain tasks from the master, and the size of each task is equalized, good 
   load balancing is achieved. 

In this system, generator and subsumption processes run in a demand-
driven mode, while tester processes run in a data-driven mode. 

The main factor in the degradation of system performance is sequentiality in 
subsumption testing. This can be minimized by utilizing the synchronization 
mechanism supported by KL1. Demand-driven control can also be easily and 
efficiently implemented by utilizing the KL1 stream. 

By using demand-driven control, we can not only suppress unnecessary 
model extensions and subsumption tests but also maintain the high running 
rate which is the key to achieving linear speedup. 

- 69 -

MGTP Applications (1) 
Abductive Reasoning System 

Abstract 

We have developed several parallel abductive reasoning systems using the 
MGTP. We will describe two implementations of the abductive reasoning 
system shown in Figure 1: one is the MGTP+MGTP method, and the other 
is the Skip method. In each method, the given input formulas are translated 
into MGTP rules in a different way. We demonstrated them by applying them 
to a logic circuit design problem. 





Figure 1: Abductive Reasoning System based on the MGTP 

Abduction 

We considered the first-order abductive framework (~),r), where ~D is a 
set of Horn clauses and r is a set of atoms (abducibles). A set E of ground 
instances of elements of r is an explanation of a closed formula G from (~], r) 
if: (1) ~~ U E ~ G, and (2) ~ U E is consistent. Given ~), r and G, the task 
of abduction is to find the explanations of G from (~, r). 

MGTP+MGTP 

Each ground hypothesis H from r is represented by fact(H, {H}), and each 
Horn clause in ~ of the form: 

A1 A . . . A An D C, 

is translated into the MGTP rule of the form: 

fact(A1 E1),..., fact(An, En) -> fact(C, cc( ~ Ei )), 
i= 1 

- 71 -

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

cc(E) E if ~ U E is consistent; 
nil otherwise. 

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. 




Figure 2: MTGP+MTGP

Skip Method 

When a clause in ~] contains the negative occurrences of abducibles H1 ' ' ' " Hm 
(Hi e r, m ~ O) and is in the form: 

A1 A . . . A Al A H1 A . . . A Hm D C, 
abducibles

we translate it into the following MGTP rule: 

A1,...,Al -> H1,...,Hm, C | -KH1 |  ¥ ¥ | *KHm. 

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 -KH is rejected by the schema: 

-KH, H -> for every hypothesis H. 

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 -

MGTP Applications (2) 
Protocol Specification Description System 

Abstract 

In order to describe a complex protocol specification easily, we proposed 
a protocol specification description language, Ack. We developed a process-
ing system for this language using the parallel theorem proving technique, 
and applied it to the description of several services for a telephone switching 
system. 

Ack Notation 
¥ Atomic Formulas 






¥ Clause (A1 A... A Am -> B1 A... A Bn) 





Axioms for Ack 
¥ Synchronization 





- 73 -