RUI: Applications of Classical Inference Techniques to Multiple-Valued Logics and to Prime Implicate Algorithms

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

This project is for research in computational logic. The areas of research stem directly from prior analysis of the structure formulas in negation normal form. That work raised many questions and led to explorations in several directions. Substantial results at the propositional level, preliminary experimental at the first order level, and certain theoretical results that the most important of these may be path dissolution, a rule of inference that is strongly complete at the ground level. This project continues exploration of this and related inference mechanisms, largely through experimentation. One major thrust is to further the implementation of the techniques developed earlier. The current first order system (``Dissolver'') is a solid platform on which the following techniques may 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 investigations into multiple-valued logics largely fit the category; the study of the following issues contributes to the development of Dissolver: dissolution and multiple-valued logics; dissolution, analytic tableaux, and distributive law; quantifier duplication, proof length, and cycles; algorithms for computing prime implicants; and induction and equality.