RUI: Deduction in Classical and Multiple-Valued Logics

这个项目研究了与多值逻辑的定理证明技术和证明完备性有关的几个领域：-最重要的工作可能是一种新的推理规则，一种类似解析的规则，暂定为规则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.