alpha-Quasi-Lock Semantic Resolution Method Based on Lattice-Valued Logic

作者：Zhong Xiaomei^*; Xu Yang; Liu Jun; Chen Shuwei

来源：International Journal of Computational Intelligence Systems, 2014, 7(3): 418-431.

DOI：10.1080/18756891.2013.859868

• alpha -Quasi-lock semantic resolution method
• resolution-based automated reasoning
• general form of -resolution principle
• lattice-valued logic
• lattice implication algebra

Based on the general form of -resolution principle for a lattice-valued logic with truth-values defined in a lattice-valued logical algebra structure - lattice implication algebra, the further extended -resolution method in this lattice-valued logic is discussed in the present paper in order to increase the efficiency of the resolution method. Firstly, -quasi-lock semantic resolution method in lattice-valued propositional logic LP(X) is established by combining the lock and semantic resolution simultaneously, and its theorems of soundness and conditional completeness are proved. Secondly, this -quasi-lock semantic resolution method is extended into the corresponding lattice-valued first-order logic LF(X), and its soundness and conditional completeness are also established. This extended resolution method will provide a theoretical basis for automated soft theorem proving and program verification based on lattice-valued logic.

• 出版日期2014
• 单位西南交通大学