MULTI-ARY α-SEMANTIC RESOLUTION AUTOMATED REASONING BASED ON A LATTICE-VALUED PROPOSITION LOGIC LP(X)

摘要

This paper focuses on multi-wry α-semantic resolution automated reasoning method based on multi-ary α-resolution principle for lattice-valued propositional logic LP(X) with truth-value in lattice implication algebras. The definitions of the multi-ary α-semantic resolution and multi-ary α-semantic resolution deduction in lattice-valued propositional logic LP(X) are given, respectively, and the soundness and completeness are gotten. An algorithm of multi-ary α-semantic resolution method is constructed; the soundness and completeness of multi-ary α-semantic resolution algorithm are also obtained. This work will provide a theoretical foundation for the more efficient resolution based automated reasoning in lattice-valued logic.