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 -