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.

这是计算逻辑中的研究项目。 研究领域直接源于对公式对几个研究主题的否定结构的分析。 在命题水平上的实验结果，一阶级别的初步实验结果，并且某些理论结果表明，其中最重要的可能是路径溶解，这是在地面上强烈完成的推理规则。 对此和相关推理机制的探索将主要通过实验继续。 调查的一个主要目的是进一步实施路径分辨率和语义图技术。 现在是一个复杂的地面系统和一阶系统的运行；后者是一个可靠的平台，将在下面提出的技术进行测试：链接选择；计算主要隐含物；回溯理论联系和解散；和星链。 尽管抽象证明理论问题本身就是感兴趣的，但定理证明系统的绩效增强的发展也是主要动机。 将研究许多此类增强功能。 其中包括：改善现有推理机制的效率；通过现有机制进行改进的证明搜索；以及开发改变搜索空间本身的新推理技术。 具体而言，将通过研究以下研究来增强系统的开发：溶出，分析表和分配定律；溶解与分辨率；量词重复，证明长度和周期；计算主要隐含物的算法；以及归纳和平等。