α-generalized Lock Resolution Automated Reasoning For Linguistic Truth-valued Lattice-valued Logic Based On Lattice Implication Algebras

Intelligent Transport Systems (ITS) is a new and complex traffic and transportation system, ulitizing advanced information techniques, intelligent techniques and social knowledge, which has variety of uncertain information. Resolution automated reasoning in many-valued logic is an important research direction for dealing with many kinds of complex uncertain information especially for transportation. In ITS, the research of incomparable and linguistic valued information, and the formal verification of related software and hardware systems are the most basic and critical one, which provides the intelligent information processing theories and methods, and designs the intelligent computing or inference systems for transportation.Based on the extensive work of a-resolution automated reasoning in linguistic truth-valued lattice-valued logic, the dissertation discusses the structure and its a-resolvability of the generalized literal. For further improving the efficiency of a-resolution, a-lock resolution is proposed as well as its soundness, completeness, and universal algorithm. Meanwhile, it is realized on the computer by Matlab. Furthermore, a-generalized resolution is introduced in linguistic truth-valued lattice-valued logic. a-Generalized lock resolution is discussed in details including its theories, methods, algorithms and procedures. Concretely, the contents of the dissertation include the following four aspects.1. The universal methods for finding all κ-IESFs and judging the α-resolvability of κ-IESFs are given in LV(n×2)P(X). Concretely, some operational properties among the logical formulae in L6P(X) are studied. An algorithm is contrived for finding all κ-IESFs in L6P(X). Then all the results in L6P(X) are extended to LV(n×2)P(X), and a unified algorithm for finding all κ-IESFs in LV(n×2)P(X) is proposed. Furthermore, from the semantic view, the normal properties of two traditional formulae, i.e., F=F1â†'F2and F=(F1â†'F2)’, are discussed. A universal method for validating a-resolvability of formulae in LnP(X) is also studied.2. α-Lock resolution method and its compatibilities are discussed in LV(n×2)F(X). Concretely, α-lock resolution methods for LP(X) and LF(X) are discussed in details including the concepts, properties, soundness and weak completeness, and the reasoning algorithms. The transformation of α-lock resolution between LV(n×2)F(X) and LnP(X), and α-satisfiability of logical formulae are discussed. The concepts of α-unit resolution and α-input resolution are introduced, their soundness and completeness are also established. Four hybrid resolution methods are shown by combining α-lock resolution with generalized deleting strategy, α-linear resolution, α-unit resolution, and α-input resolution in LnF(X).3.α-Generalized resolution principle is studied including its concepts, soundness and completeness in LV(n×2)F(X). The a-unsatisfiability of logical formulae are discussed. The equivalence of a-generalized resolution between LV(n×2)F(X) and LnP(X) is also given.4. a-Generalized lock resolution method for LP(X) and LF(X) is discussed in details including the concepts, properties, soundness and weak completeness. The transformation of a-generalized lock resolution between LV(n×2)F(X) and LnP(X) is given. The compatibility of a-generalized lock resolution with α-generalized linear resolution is discussed. The comparisons among a-generalized lock resolution and other three typical resolution methods are also analyzed from the validity, complexity and practicability.