Linear Input Theorem Provers: Design & Performance Enhancement

本次更新项目将继续对模型进行调查 消除（ME）程序。 ME程序，一个线性输入证明 程序，最近由于几个原因受到关注， 包括使用优雅的Prolog实现的能力 建筑 以前的工作通过实施表明， ME在一个有趣的集合上比其他统一证明器有优势 困难的问题。 新的调查将试图克服 ME程序的严重缺陷，没有使用中间结果， 而不破坏我所享有的速度优势。 比如说 选择性的性质，引理使用ME邀请高度选择性 Lemma保留机制。 另一种方法允许低 选择性，但不太可能获得高增益。 工作将 也继续发展顺序，并行和 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.