Determination of alpha-resolution in lattice-valued first-order logic LF(X)

作者：Xu Yang; Liu Jun^*; Ruan Da; Li Xiaobing

来源：Information Sciences, 2011, 181(10): 1836-1862.

DOI：10.1016/j.ins.2010.03.024

• Incomparability
• Many-valued logic
• Automated reasoning
• Lattice implication algebra
• Lattice-valued logic
• alpha-Resolution

Key issues for resolution-based automated reasoning in lattice-valued first-order logic LF(X) are investigated with truth-values in a lattice-valued logical algebraic structure lattice implication algebra (LIA). The determination of resolution at a certain truth-value level (called alpha-resolution) in LF(X) is proved to be equivalently transformed into the determination of alpha-resolution in lattice-valued propositional logic LP(X) based on LIA. The determination of alpha-resolution of any quasi-regular generalized literals and constants under various cases in LP(X) is further analyzed, specified, and subsequently verified. Hence the determination of alpha-resolution in LF(X) can be accordingly solved to a very broad extent. which not only lays a foundation for the practical implementation of automated reasoning algorithms in LF(X). but also provides a key support for alpha-resolution-based automated reasoning approaches and algorithms in LIA based linguistic truth-valued logics.

• 出版日期2011-5-15
• 单位西南交通大学; 东北财经大学