α-Resolution Method for Lattice-valued Horn Generalized Clauses in Lattice-valued Propositional Logic Systems

被引：3

作者：

Xu, Weitao ^{[1
]}

Zhang, Wenqiang ^{[1
]}

Zhang, Dexian ^{[1
]}

Xu, Yang ^{[2
]}

Pan, Xiaodong ^{[2
]}

机构：

[1] Henan Univ Technol, Coll Informat Sci & Engn, Zhengzhou 450001, Peoples R China

[2] Southwest Jiaotong Univ, Sch Math, Chengdu 610031, Peoples R China

来源：

INTERNATIONAL JOURNAL OF COMPUTATIONAL INTELLIGENCE SYSTEMS | 2015年 / 8卷

基金：

国家高技术研究发展计划(863计划); 中国国家自然科学基金;

关键词：

automated reasoning; lattice-valued logic; alpha-resolution; lattice-valued Horn g-clause; lattice implication algebra;

D O I：

10.1080/18756891.2015.1129580

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

In this paper, an -resolution method for a set of lattice-valued Horn generalized clauses is established in lattice-valued propositional logic system L P(X ) based on lattice implication algebra. Firstly, the notions of lattice-valued Horn generalized clause, normal lattice-valued Horn generalized clause and unit lattice-valued Horn generalized clause are given in L P(X ). Then, the -resolution of two lattice-valued Horn generalized clauses is represented in L P(X ). It indicates the reasoning rules in a resolution process, which aims at deleting -resolution literals and obtaining a resolvent. Finally, we build an -resolution algorithm for a set of lattice-valued Horn generalized clauses in L P(X ). It provides a foundation for automated reasoning in lattice-valued first-order logic system and an application for designing an inference system in the field of intelligent decision support.

引用

页码：75 / 84

页数：10

共 16 条

[1]

[Anonymous], 1973, Symbolic Logic and Mechanical Theorem Proving, DOI DOI 10.1137/1016071

[2] A resolution-like strategy based on a lattice-valued logic [J].

Liu, J ;

Ruan, D ;

Xu, Y ;

Song, ZM .

IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2003, 11 (04) :560-567

[3]

Liu J, 2000, NINTH IEEE INTERNATIONAL CONFERENCE ON FUZZY SYSTEMS (FUZZ-IEEE 2000), VOLS 1 AND 2, P191, DOI 10.1109/FUZZY.2000.838657

[4]

LIU XH, 1994, RESOLUTION BASED AUT

[5]

Loveland D. W., 1978, Automated theorem proving: a logical basis. Fundamental studies in computer science

[6]

Pei Z., 2010, LINGUISTIC VALUES BA, VVolume 259

[7]

Qin K. Y., 1994, Journal of Southwest Jiaotong University, V1, P22

[8] A MACHINE-ORIENTED LOGIC BASED ON RESOLUTION PRINCIPLE [J].

ROBINSON, JA .

JOURNAL OF THE ACM, 1965, 12 (01) :23-&

[9] Automatic Web service composition based on Horn clauses and Petri nets [J].

Tang, Xianfei ;

Jiang, Changjun ;

Zhou, Mengchu .

EXPERT SYSTEMS WITH APPLICATIONS, 2011, 38 (10) :13024-13031

[10] α-resolution principle based on lattice-valued propositional logic LP(X) [J].

Xu, Y ;

Ruan, D ;

Kerre, EE ;

Liu, J .

INFORMATION SCIENCES, 2000, 130 (1-4) :195-223

← 1 2 →