Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra |
| |
| Authors: | Wei-tao Xu Yang Xu |
| |
| Institution: | [1]Intelligent Control Development Center, Southwest Jiaotong University, Chengdu 610031, China; [2]Department of Mathematics, Southwest Jiaotong University, Chengdu 610031, China; [3]College of Information Science and Engineering, Henan University of Technology, Zhengzhou 450001, China |
| |
| Abstract: | As a continuate work, ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed, which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra. In this principle, the resolution
level is an ideal of lattice implication algebra, instead of an element in truth-value field. Moreover, the soundness theorem
is given. In the light of lifting lemma, the completeness theorem is established. This can provide a new tool for automated
reasoning. |
| |
| Keywords: | automated reasoning lattice-valued logic lattice implication algebra generalized clause |
| 本文献已被 CNKI 维普 SpringerLink 等数据库收录！ |
|
