α-Generalized Linear Resolution Method Based on Lattice-Valued Propositional Logic LP(X)
The aim of this paper is to provide a more efficient approach for resolution-based automated reasoning in lattice-valued logic system. In the present paper, an a-generalized linear resolution method for latticevalued propositional logic system LP(X) based on lattice implication algebra is established. Firstly, the properties of a-generalized resolution in lattice-valued propositional logic system are discussed. Secondly, some concepts for the ageneralized linear resolution method are presented. Both the soundness and weak completeness theorems for the a-generalized linear resolution method in LP(X) are investigated. The proposed approach efficiently deals with unsatisfiability under a truth-valued level a for a set of the general g-clauses in lattice-valued propositional logic system. This study can be expected to provide objective basis in order to design an applied automated reasoning program in the intelligent reasoning system.
automated reasoning lattice implication algebra lattice-valued logic general g-clause generalized linear resolution
Weitao Xu Yang Xu
Intelligent Control Development Center Southwest Jiaotong University Chengdu 610031, China School of Mathematics Southwest Jiaotong University Chengdu 610031, China
国际会议
上海
英文
1466-1470
2011-07-26（万方平台首次上网日期，不代表论文的发表时间）