RUI: Deduction in Classical and Multiple-Valued Logics

本项目考察了与多值逻辑（MVL）和证明完备性的定理证明技术相关的几个研究领域：-最重要的工作可能是一个新的推理规则，一个暂定名为修改的类解析规则，用于规则MVL。修正算法似乎比现有的MVL推断方法更有效；也有可能修改提供的见解可以用于改进其他MVL推理规则的搜索行为。符号逻辑是经典逻辑的一种改编，用于MVL的推理。最近为有符号逻辑开发了几个适度的实现。目前的项目将把重点扩大到一般定理证明设置中的实现。也将进行逻辑编程和约束求解的实验。-注释逻辑对应于自然产生的一类签名逻辑，并已应用于不一致推理。当前的注释逻辑系统在认知不一致方面是副一致的，也就是说，不一致容忍，但它们在本体论不一致方面的行为是经典的。定义了符号逻辑到标注逻辑的映射，将本体不一致映射为认知不一致。在提议的项目中对这种映射的属性进行进一步的调查，有望对两个不一致概念之间的关系产生富有成效的见解。-最近推广了Anderson-Bledsoe解决的完备性的过量文字证明，以提供已知结果的简化证明，以及证明NNF公式的连通表和连通正则表的完备性和线性非子句解决的完备性。该项目将审查该技术在其他证明程序方法中的应用。

This project examines several areas of research related to theorem proving techniques for multiple-valued logics (MVL's) and for proving completeness: - The most important work may be a new rule of inference, a resolution-like rule tentatively named Modification, for regular MVL's. It appears likely that Modification is more effective than existing methods of inference for MVL's; it is also likely that the insights provided by Modification can be adapted to improve the search behavior of other MVL inference rules. - Signed logic is an adaptation of classical logic for reasoning about MVL's. Several modest implementations have been developed recently for signed logic. The current project will broaden the focus to implementations in the general theorem proving setting. Experiments with logic programming and constraint solving will also be undertaken. - Annotated logic corresponds to a naturally arising class of signed logic and has been applied to reasoning with inconsistency. Current systems of annotated logic are paraconsistent, that is, inconsistency tolerant, with respect to epistemic inconsistency, but they behave classically with respect to ontological inconsistency. A mapping from signed logic to annotated logic has been defined which has the effect of mapping ontological inconsistency to epistemic inconsistency. Further investigation into properties of this mapping in the proposed project is expected to lead to fruitful insights on the relationships between the two notions of inconsistencies. - The Anderson-Bledsoe excess literal proof of the completeness of resolution was recently generalized to provide simplified proofs of known results as well as to prove completeness of connected tableaux and of connected regular tableaux for NNF formulas and the completeness of linear non-clausal resolution. The project will examine the application of the technique to still other methods of proof procedures.