RUI: Deduction in Classical and Multiple-Valued Logics

点击翻译按钮获取中文摘要

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.