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.