(5) Parallelization of PROGOL in KL1

We are designing and implementing PROGOL by using MGTP technology which is a theorem proving method based on a bottom-up inference called model generation. Specifically, in the new design, MGTP technology is applied in a more elegant manner than the original to the computation of most specific hypothesis that is deduced from background knowledge and the negation of a positive example. MGTP technology is also being applied to the calculation of the cover set, a set of positive examples covered by generated hypotheses, which is the most essential computation for obtaining better hypotheses to explain given positive examples. Since MGTP already has very efficient parallel implementations on parallel inference machines, an efficient implementation of parallelized PROGOL will readily be realized as well.