The Study Of Resolution Automated Reasoning For Linguisitc Truth-Valued Lattice-Valued Logic

An outstanding problem in Artificial Intelligence is how to deal with uncertainty information.To realize the reasoning under uncertainty,much of the research has been concentrated on resolution-based theories and methods for lattice-valued logic system.On the other hand,since human actions are always involved with uncertainty information processing,and uncertainty information is described by natural language,to investigate theories and methods of uncertainty information processing described by natural languages in Artificial Intelligence is not only necessary but also critical.Based on previous internal and external outcome of researches in these directions for reference,the research presented in this thesis focuses onα-resolution,resolution-based automated reasoning methods and its algorithms for linguistic truth-valued lattice-valued logic and decision making methods based on lattice implication algebra.The specific contents are as follows:Part One Study on resolution of linguistic truth-valued lattice-valued propositional logic system LVL_n×2P(X)1.The properties ofα-resolution fields of LP(X) are presented.2.The properties of J - resolution fields of LP(X) are given.3.The relations betweenα-resolution and J-resolution of LVL_n×2P(X) are discussed in details.Part Two Study onα-resolution fields of lattice-valued propositional logic L_nP(X)α-resolution fields of 0-IESF,1-IESF and 2-IESF of L_nP(X) are given and conditions for determining if two generalized literals areα-resolution pair are obtained.Part There Study onα-resolution automated reasoning methods of linguistic truth- valued lattice-valued propositional logic system 1.Anα-automated reasoning method,algorithm and its flow chart of LVL_nP(X) are presented.2.Anα-automated reasoning method and algorithm of LVL₉P(X) are provided,its soundness and completeness are proved,and the computational complexity of the algorithm is analyzed.3.An M-automated reasoning method and algorithm of L_2n+1P(X) based on sub-regular generalized literals are given and its soundness and completeness are proved.Part Four Study on algorithm for finding ground instances of simple generalized clause set in lattice-valued first-order logic LF(X)1.The unification algorithm of LF(X) is given.2.An algorithm for finding ground instances of simple generalized clause set oi LF(X) is given and its soundness and completeness are proved.Part Five Study on decision making based on linguistic-valued lattice implication algebra1.A method of multi-objective decision making based on linguistic-valued lattice implication algebra is presented.2.A method of multi-objective decision making with general lattice information is presented.3.A method of group decision making with qualitative and quantitative information is presented.