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

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

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.