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

该项目继续一项研究计划， 逻辑 研究的研究领域直接源于一个 否定范式公式的结构分析 对多值逻辑的研究。 前一项工作导致了 发展出一种叫做路径分解的演绎规则。 研究 继续，包括研究其属性作为一个 推理机制和一个可移植的C++实现的发展。 为 一段时间以来，似乎解散将是一个有用的工具， 设计素蕴涵/蕴涵算法。 一种新的否定范式 (NNF)算法，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.