Bottom-up abduction by model generation

Abstract

We investigate two realizations of parallel abductive reasoning systems using the model generation theorem prover MGTP. The first one, called the MGTP+MGTP method, is a co-operative problem-solving architecture in which model generation and consistency checking communicate with each other. There, parallelism is exploited by checking consistencies in parallel. However, since this system consists of two different components, the possibilities for parallelization are limited. In contrast, the other method, called the Skip method, does not separate the inference engine from consistency checking, but realizes both functions in only one MGTP that is used as a generateand-test mechanism. In this method, multiple models can be kept in distributed memories, thus a great amount of parallelism can be obtained. We also attempt the upside-down metainterpretation approach for abduction, in which top-down reasoning is simulated by a bottomup reasoner. 1