Building a Distributed Knowledge Information System Based on Model Generation

我们开发了一个基于并行模型生成的定理证明系统MGTP，该系统具有高效的证明搜索和成功应用的新技术。我们还开发了CMGTP（约束MGTP）来处理约束满足问题。通过实现带负原子的约束传播，与原始MGTP相比，CMGTP可以将搜索空间减少几个数量级。为了提高对搜索空间的剪枝能力，我们开发了一种新的方法，称为非霍恩魔术集（NHM），并将其相关性测试功能整合到Letz提出的折叠（FU）方法中。NHM方法抑制了与目标无关的子句的无用模型生成。FU方法避免了在分例后产生重复子证明。利用这些方法，我们可以消除基于模型生成的定理证明中的两种主要的冗余。针对并行程序在运行时产生大量任务的并行机器，提出了一种有效的并行执行方法。在这种方法中，同时激活的任务数被限制在最多N个，超过创建的任务数将被挂起，直到允许它们被激活，从而依次进行处理。我们在并行推理机PIM/m （128PE）和共享内存并行机Cray SuperServer6400 （20PE）上实现了用并发编程语言KL1编写的并行定理证明系统MGTP的方法。结果表明，通信开销显著降低，实现了显著的加速。研究了基于遗传算法的启发式证明搜索。

We have developed a parallel model-generation based theorem-proving system MGTP with novel techniques for efficient proof-search and successful applications.We have also developed CMGTP (Constraint MGTP) to deal with constraint satisfaction problems. By attaining the constraint propagation with negative atoms, CMGTP makes it possible to reduce search spaces by orders of magnitude compared to the original MGTP.To enhance the ability to prune search spaces, we have developed a new method called non-Horn magic sets (NHM) and incorporated its relevancy testing function into the folding-up (FU) method proposed by Letz. The NHM method suppresses useless model generation with clauses irrelevant to the goal. The FU method avoids generating duplicated subproofs after case-splitting. With these methods we can eliminate two major kinds of redundancies in model-generation based theorem provers.An efficient parallel execution method is presented for parallel programs which create many tasks at runtime on parallel machines with N number of processing elements (PEs) available at any time. In this method, the number of tasks activated at the same time is limited to at most N, and the exceeding number of created tasks are suspended until they are allowed to be activated, thus being processed sequentially. We implemented the method for the parallel theorem proving system MGTP written in the concurrent programming language KL1 running on the parallel inference machine PIM/m (128PE) as well as the shared-memory parallel machine Cray SuperServer6400 (20PE). The results show remarkable reduction of communication overhead achieving significant speedup.We have studied heuristic proof-search based on the genetic algorithm.