Implementation and Analysis of Proof Techniques Employing Negation Normal Form

否定范式证明技术的实现与分析

• 批准号: 9101208
• 负责人: Neil Murray
• 金额: $ 17.19万
• 依托单位: SUNY at Albany
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-06-01 至 1995-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9101208&HistoricalAwards=false
• 关键词: Implementation; Analysis; Proof; Techniques; Employing

This is a research project in computational logic. The areas of research stem directly from the analysis of the structure of formulas in negation toward several research topics. Substantial experimental results at the propositional level, preliminary experimental results at the first order level, and certain theoretical results indicate that the most important of these may be path dissolution, a rule of inference that is strongly complete at the ground level. Exploration of this and related inference mechanisms will be continued, largely through experimentation. One major thrust of the investigation will be to further the implementation of the path resolution and semantic graph techniques developed earlier. A sophisticated ground system and a first order system are now operational; the latter is a solid platform on which techniques proposed below will be tested: link selection; computing prime implicants; backtracking; theory links and dissolution; and star chains. While abstract proof-theoretic questions are of interest in their own right, the development of performance enhancements for the theorem proving system is also a major motivation. A number of such enhancements will be investigated. Among them are: improved efficiency of existing inference mechanisms; improved proof search with existing mechanisms; and development of new inference techniques that alter the search space itself. Specifically, system development will be enhanced through investigation of: dissolution, analytic tableaux, and the distributive law; dissolution versus resolution; quantifier duplication, proof length, and cycles; algorithms for computing prime implicants; and induction and equality.

这是一个计算逻辑的研究项目。 领域 研究直接源于对公式结构的分析 对几个研究课题的否定。 实质性实验 在命题水平上的结果，初步实验结果 在一阶水平上，某些理论结果表明， 其中最重要的可能是路径分解， 在基础水平上强完备的推理。 探索 这一点和相关的推理机制将继续下去，主要是 通过实验。 调查的一个主要目的是进一步推动 路径解析和语义图技术的实现 开发较早。 一个复杂的地面系统和一个 系统现已投入运行;后者是一个坚实的平台， 下面提出的技术将被测试：链接选择;计算 主蕴涵;回溯;理论联系与消解; 星星链。 虽然抽象的证明理论问题本身很有趣， 对，开发性能增强定理 证明制度也是一个重要的动机。 许多这样的 将研究改进措施。 其中包括：改善 现有推理机制的效率;改进的证明搜索 现有机制;以及发展新的推理技术 改变搜索空间本身。 具体而言，将通过以下方式加强系统开发： 研究：溶出度、分析表和 分配律;分解与消解;量词 重复、证明长度和循环;计算素数的算法 蕴涵;归纳和平等。