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

Research output: Contribution to journalArticlepeer-review


Institutes & Expert groups

  • Southwest Jiaotong University
  • Ulster University - Faculty of Computing and Engineering
  • DUFE - Dongbei University of Finance and Economics

Documents & links


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 α-resolution) in LF(X) is proved to be equivalently transformed into the determination of α-resolution in lattice-valued propositional logic LP(X) based on LIA. The determination of α-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 α-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 α-resolution-based automated reasoning approaches and algorithms in LIA based linguistic truth-valued logics.


Original languageEnglish
Pages (from-to)1836-1862
Number of pages27
JournalInformation Sciences
Issue number10
Publication statusPublished - 15 May 2011


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

ID: 6856416