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

该项目继续了逻辑方面的研究计划。研究领域直接来源于对否定范式公式结构的分析和对多值逻辑的研究。前人的工作导致了称为路径分解的演绎规则的发展。继续的研究，包括将其作为推理机制的属性的研究，以及可移植C++实现的开发。一段时间以来，消解似乎是设计主蕴涵/蕴涵算法的一个有用的工具。为此，发展了一种新的可与分解相结合的否定范式算法PI，并发现了基于CNF/DNF的方法难以实现但易于进行PI/分解的公式类。一个原型系统已经实现，并正在进一步开发中。这些技术正在扩展到多值逻辑(MVL)。MVL的工作还包括研究带注释的逻辑编程和SLD风格的证明过程，以及模糊逻辑的推理方法。

This project continues a research program in logic. The studied areas of research stem directly from an analysis of the structure of formulas in negation normal form and from investigations into multiple-valued logics. The former work led to the development of the deduction rule called path dissolution. The study of continues, including the study of its properties as an inference mechanism and the development of a portable C++ implementation. For some time it has appeared that dissolution would be a useful tool in the design of prime implicant/implicate algorithms. A new negation normal form (NNF) algorithm, PI, has been developed that can be combined with dissolution for this purpose, and formula classes have been discovered that are hard for CNF/DNF-based methods but that are easy for PI/dissolution. A prototype system has been implemented and is being further developed. These techniques are being extended to multiple-valued logics (MVL's). The work in MVL's also includes the study of annotated logic programming and SLD-style proof procedures, and inference methods for fuzzy logics.