On α-Quasi-Lock Semantic Resolution Automated Reasoning Based On Lattice-Valued Logic

Intelligent traffic system is a new type of complex transport systems, which integrates information, intelligence and society. There must be a lot of various and complex uncertain information occurring in intelligent traffic system. To deal with these uncertain information more reasonably, we need logic as its theoretical basis. Due to the complexity of intelligent traffic system, there must be a lot of information described by linguistic values and a variety of software systems occurring in this system. Therefore, it is a cutting-edge basic research direction that using automated reasoning based on logic to deal with the incomparability, linguistic values and correctness of the corresponding software systems in intelligent traffic system.Lattice-valued logic is a kind of important multi-valued logic, and it can describe both the information with comparablility and the information with incomparablility simultaneously. The aim of this paper is to establish the automated reasoning method based on gradational resolution principle in lattice-valued logic system with truth-value in lattice implication algebras, analyze the corresponding resolution automated reasoning method in linguistic truth-valued lattice-valued logic based on linguistic truth-valued lattice implication algebra further, and construct the corresponding resolution automated reasoning algorithm. The main content of this paper is as follows.The forms of all subregular and non-subregular3-order indecomposable extremely simple form in lattice-valued propositional logic LnP(X) based on Lukasiewicz implication algebra Ln are gave out. And then the forms of all3-order indecomposable extremely simple form in LnP(X) are obtained. On this basis, the determination of a-resolution between a class of3-order indecomposable extremely simple form and the0-order,1-order,2-order,3-order indecomposable extremely simple form in LnP(X) is analyzed respectively.The general form of a-resolution principle is analyzed in linguistic truth-valued lattice-valued logic based on linguistic truth-valued lattice implication algebra. Without losing generality, the general form of a-resolution principle in lattice-valued propositional logic (Ln×L2)P(X) is equivalently transformed into that in lattice-valued propositional logic LnP(X). Similar equivalence is also established between the general form of a-resolution principle in linguistic truth-valued lattice-valued propositional logic LV(n×2)P(X) and that in lattice-valued propositional logic LVnP(X). The general form of a-resolution principle in lattice-valued first-order logic (Ln×L2)F(X) is equivalently transformed into that in LnP(X). Similar equivalence is also obtained between the general form of a-resolution principle in linguistic truth-valued lattice-valued first-order logic LV(n×2)F(X) and that in LVn(X).α-Quasi-lock semantic resolution method is established in lattice-valued logic system based on lattice implication algebras, and the corresponding algorithm is also designed. On the basis of the general form of a-resolution principle, α-quasi-lock semantic resolution method is proposed in lattice-valued propositional logic system LP(X) based on lattice implication algebras, and its soundness and weak completeness theorems are also proved. Afterwards, α-quasi-lock semantic resolution in lattice-valued propositional logic (Ln×L2)P(X) is equivalently transformed into that in LnP(X). Similar result is obtained between α-quasi-lock semantic resolution in linguistic truth-valued lattice-valued propositional logic LV(n×nx2)P(X) and that in lattice-valued propositional logic LVnP(X). On this basis, an a-quasi-lock semantic resolution algorithm based on LV(n×2)P(X) is designed. Furthermore, α-quasi-lock semantic resolution method based on LP(X) is extended into the corresponding lattice-valued first-order logic system LF(X), and it soundness and weak completeness are also established in LF(X). Afterwards, α-quasi-lock semantic resolution satisfying certain conditions based on lattice-valued first-order logic (Ln×L2)F(X) is also equivalently transformed into that in LnP(X). Similar result is obtained between α-quasi-lock semantic resolution in inguistic truth-valued lattice-valued first-order logic LV(n×2)F(X) and that in LVnP(X). Based on LF(X), an algorithm to find the ground instance of a logical formula is designed. Moreover, combing the a-quasi-lock semantic resolution algorithm in LV(n×2)P(X), an a-quasi-lock semantic resolution algorithm in LV(n×2)F(X) is obtained.a-Group quasi-lock semantic resolution method is proposed in lattice-valued logic system based on lattice implication algebras, and the corresponding algorithm is also designed. Based on the general form of a-resolution principle, an α-group resolution principle is established in lattice-valued propositional logic system LP(X), as well as its soundness and completeness. On this basis, an α-group quasi-lock semantic resolution method is proposed in LP(X) and its soundness and weak completeness are also established. Afterwards, α-group quasi-lock semantic resolution in lattice-valued propositional logic (Ln×L2)P(X) is equivalently transformed into that in LnP(X). Similar result is obtained between the a-group quasi-lock semantic resolution in linguistic truth-valued lattice-valued propositional logic LV(n×2)P(X) and that in LVnP(X). On the basis of a-quasi-lock semantic resolution algorithm in LV(n×2)P(X), an a-group quasi-lock semantic resolution algorithm based on LV(n×2)P(X) is proposed. Furthermore, a-group resolution principle and a-group quasi-lock semantic resolution method based on LP(X) are extended into lattice-valued first-order logic system LF(X), and their soundness and weak completeness are also established in LF(X) respectively. Afterwards, in lattice-valued first-order logic (Ln×L2)F(X), α-group quasi-lock semantic resolution satisfying certain conditions is equivalently transformed into that in LnP(X). Similar result is obtained between a-group quasi-lock semantic resolution in linguistic truth-valued lattice-valued first-order logic LV(n×2)F(X) and that in LVnP(X). Based on the α-quasi-lock semantic resolution algorithm in LV(n×2)F(X), an α-group quasi-lock semantic resolution algorithm in LV(n×2)F(X) is obtained.