Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra

被引：1

作者：

Xu, Wei-Tao ^{[1
,3
]}

Xu, Yang ^{[1
,2
]}

机构：

[1] Intelligent Control Development Center, Southwest Jiaotong University

[2] Department of Mathematics, Southwest Jiaotong University

[3] College of Information Science and Engineering, Henan University of Technology

来源：

Journal of Shanghai Jiaotong University (Science) | 2012年 / 17卷 / 02期

关键词：

Automated reasoning; Generalized clause; Lattice implication algebra; Lattice-valued logic;

D O I：

10.1007/s12204-012-1249-1

中图分类号：

学科分类号：

摘要：

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. © 2012 Shanghai Jiaotong University and Springer-Verlag Berlin Heidelberg.

引用

页码：178 / 181

页数：3

共 15 条

[1]

Robinson J.A., A machine-oriented logic based on the resolution principle [J], Journal of the Association for Computing Machinery, 12, 1, pp. 23-41, (1965)

[2]

Luckham D., Refinement theorems in resolution theory [C], Proceedings of IRIA Symposium Automatic Demonstration, pp. 16-21, (1968)

[3]

Chang C.L., Lee R.C.-T., Symbolic Logic and Mechanical Theorem Proving [M], (1973)

[4]

Liu X.-H., Resolution-based Automated Reasoning [M], (1994)

[5]

Wos L., Automated Reasoning: 33 Basic Research Problems [M], (1988)

[6]

Morgan C.G., A resolution principle for a class of many-valued logics [J], Logique and Analyse, 19, 74-76, pp. 311-339, (1976)

[7]

Baaz M., Fermuller C.G., Resolution-based theorem proving for many valued logics [J], Journal of Symbolic Computation, 19, 4, pp. 353-391, (1995)

[8]

Xu Y., Lattice implication algebras [J], Journal of Southwest Jiaotong University, 28, 1, pp. 20-27, (1993)

[9]

Xu Y., Liu J., Song Z.M., Et al., On semantics of Lvalued first-order logic L <sub>vfl</sub> [J], International Journal of General Systems, 29, 1, pp. 53-79, (2000)

[10]

Xu Y., Song Z.M., Qin K.Y., Et al., Syntax of Lvalued first-order logic L <sub>vfl</sub> [J], International Journal of Multiple-Valued Logic, 7, pp. 213-257, (2001)

← 1 2 →