RUI: Implementation and Analysis of Inference Techniques for Classical and Multiple-Valued Logics

RUI：经典和多值逻辑推理技术的实现和分析

• 批准号: 9202013
• 负责人: Erik Rosenthal
• 金额: --
• 依托单位: University of New Haven
• 依托单位国家: 美国
• 项目类别: Continuing grant
• 财政年份: 1992
• 资助国家: 美国
• 起止时间: 1992-06-01 至 1996-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9202013&HistoricalAwards=false
• 关键词: RUI; Implementation; Analysis; Inference; Techniques

This project is for research in computational logic. The areas of research stem directly from prior analysis of the structure of formulas in negation normal form. That work raised many questions and led to explorations in several directions. 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. This project will continue exploration of this and related inference mechanisms, largely through experimentation. One major thrust will be to further the implementation of the techniques developed earlier. The current first order system ("Dissolver") is a solid platform on which the techniques proposed below can 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, enhancing the performance of Dissolver is an important motivation for the theoretical work in this project. The planned investigations into multiple-valued logics largely fit the former category; the expectation is that the study of the following issues will contribute to the development of Dissolver: dissolution and multiple-valued logics; dissolution, analytic tableaux, and the distributive law; quantifier duplication, proof length, and cycles; algorithms for computing prime implicants; and induction and equality.

这个项目是在计算逻辑的研究。研究领域直接源于对否定范式公式结构的先验分析。这项工作提出了许多问题，并导致在几个方向进行探索。在命题水平上的大量实验结果，在一阶水平上的初步实验结果，以及某些理论结果表明，其中最重要的可能是路径溶解，推理规则，是强完整的基础水平。这个项目将继续探索这一点和相关的推理机制，主要是通过实验。一个主要的推动力将是进一步实施早先开发的技术。当前的一阶系统（“溶解器”）是一个坚实的平台，在其上可以测试下面提出的技术：链接选择;计算素蕴涵;回溯;理论链接和溶解;和星星链。虽然抽象的证明理论问题本身就很有趣，但提高Dissolver的性能是这个项目中理论工作的重要动机。对多值逻辑的计划研究很大程度上符合前一类;期望是对以下问题的研究将有助于溶解器的发展：溶解和多值逻辑;溶解，分析tableaux和分配律;量词复制，证明长度和循环;计算素蕴涵的算法;归纳和等式。