Non-clausal multi-ary alpha-generalized resolution calculus for a finite lattice-valued logic

Yang Xu, J. Liu, Xingxing He, Xiaomei Zhong, Shuwei Chen

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)
87 Downloads (Pure)


Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α-resolution), a non-clausal multi-ary α-generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.
Original languageEnglish
Pages (from-to)384-401
Number of pages18
JournalInternational Journal of Computational Intelligence Systems
Issue number1
Publication statusPublished (in print/issue) - 15 Jan 2018


  • Automated reasoning
  • Resolution principle
  • Lattice-valued logic


Dive into the research topics of 'Non-clausal multi-ary alpha-generalized resolution calculus for a finite lattice-valued logic'. Together they form a unique fingerprint.

Cite this