具有三种否定的模糊命题逻辑形式系统FLCOM的λ-归结

λ-Resolution of Fuzzy Propositional Logic System with Three Kinds of Negation FLCOM

考虑到模糊逻辑中定理自动证明的重要性以及目前主要研究具有一种否定的模糊逻辑的归结原理,文中对具有三种否定(矛盾否定、对立否定和中介否定)的模糊命题逻辑(FLCOM)的归结原理进行研究.基于FLCOM的一种无穷值语义解释提出λ-可满足的和λ-不可满足的概念.将λ-归结方法引入FLCOM,给出FLCOM的λ-归结演绎定义,讨论FLCOM的λ-归结原理,并证明FLCOM的λ-归结方法的完备性.基于λ-归结方法和已证明的结论给出实例以佐证文中λ-归结方法和结论的正确性和可行性.因此,在FLCOM范围内可判定任一模糊命题公式是否是λ-可满足的或λ-不可满足的.

Since the importance of automated reasoning and the resolution principle of the fuzzy logic with one negation is mainly studied now, the resolution principle of the fuzzy proposition logic （FLCOM） with three kinds of negation, contradictory negation, opposite negation and medium negation, is discussed. Based on an infinite-valued semantic interpretation of FLCOM, λ-satisfiable and λ-unsatisfiable concepts are proposed, and λ-resolution method is introduced into FLCOM. Besides,λ-resolution deduction of FLCOM is defined and λ-resolution principle of FLco~ is discussed. Moreover, the completeness of λ-resolution method is proved. Based on A-resolution method and the proved conclusions, some examples providing evidences for the λ-resolution method and the conclusions are listed below the corresponding definitions and theorems. Therefore, whether a fuzzy propositional formula is λ-satisfiable or λ-unsatisfiable can be determined in the range of FLCOM.