Linear Input Theorem Provers: Design & Performance Enhancement

该更新项目将继续调查模型消除(ME)程序。ME过程是一种线性输入证明过程，最近由于几个原因而受到关注，包括使用优雅的Prolog实现体系结构的能力。以前的工作已经通过实现证明了ME在一组有趣的困难问题上比其他统一证明者具有优势。新的调查将试图克服ME程序最严重的障碍，即不使用中间结果，而不破坏ME享有的速度优势。例如，用于ME的词条使用的可选性质导致了高度选择性的词条保留机制。另一种方法允许低选择性，但不太可能获得高收益。还将继续开发ME的顺序、并行和分布式实施。

This renewal project will continue the investigation of the Model Elimination (ME) procedure. The ME procedure, a linear input proof procedure, has received recent attention for several reasons, including the ability to use the elegant Prolog implementation architectures. Previous work has demonstrated by implementation that ME has an advantage over other uniform provers on an interesting set of hard problems. New investigation will attempt to overcome the most severe handicap of the ME procedure, no use of intermediate results, without destroying the speed advantage ME enjoys. For example, the optional nature of lemma use for ME invites highly selective mechanisms for Lemma retention. An alternate approach allows low selectivity but not as much possibility of high gains. Work will also continue on the development of sequential, parallel and distributed implementations of ME.