Linear Input Theorem Provers: Design & Performance Enhancement

线性输入定理证明器：设计

• 批准号: 9116203
• 负责人: Donald Loveland
• 金额: $ 17.16万
• 依托单位: Duke University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1992
• 资助国家: 美国
• 起止时间: 1992-02-01 至 1996-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9116203&HistoricalAwards=false
• 关键词: Linear; Input; Theorem; Provers; Design

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.

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