General Form of a-Ordered Linear Resolution Method for Lattice-Valued Logic System with Linguistic Truth-Values

被引：0

作者：

Xu, Weitao ^{[1
]}

Xu, Yang ^{[2
]}

机构：

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

[2] Southwest Jiaotong Univ, Dept Maths, Chengdu 610031, Peoples R China

来源：

2016 INTERNATIONAL CONFERENCE ON FUZZY THEORY AND ITS APPLICATIONS (IFUZZY) | 2016年

基金：

中国国家自然科学基金;

关键词：

automated reasoning; linguistic truth-valued lattice-valued logic system; ordered linear resolution; generalized literal; generalized clause;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

In the present paper, general form of alpha-ordered linear resolution method IS established m lattice-valued logic system with linguistic truth-values. Firstly, general form of alpha-ordered linear resolution method is investigated in linguistics truth-valued lattice-valued propositional logic system based on linguistics truth-valued lattice implication algebra. It can obtain a resolvent under a linguistic truth-valued level for a set of generalized clauses. Both soundness and weak completeness theorems are established. Then, general form of alpha-ordered linear resolution method IS established in linguistics truth-valued lattice-valued first-order logic system. The soundness theorem is also given. Finally, By using lift lemma, the weak completeness theorem is also obtained. This method provides a new resolution approach for automated reasoning based on lattice-valued logic system.

引用

页数：7

共 16 条

[1]

[Anonymous], 2003, STUD FUZZINESS SOFT

[2]

[Anonymous], 1978, Automated Theorem Proving: A Logical Basis

[3] RESOLUTION-BASED THEOREM-PROVING FOR MANY-VALUED LOGICS [J].

BAAZ, M ;

FERMULLER, CG .

JOURNAL OF SYMBOLIC COMPUTATION, 1995, 19 (04) :353-391

[4]

Chang C.-L., 1973, Symbolic Logic and Mechanical Theorem Proving, DOI DOI 10.1137/1016071

[5]

LIU X, 1994, RESOLUTION BASED AUT

[6]

Loveland D. W., 1970, P IRIA S AUT DEM, P147, DOI DOI 10.1007/BFB0060630

[7]

Luckham D, 1970, P IRIA S AUT DEM VER

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

ROBINSON, JA .

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

[9]

Sofronie-Stokkermans V, 2007, J MULT-VALUED LOG S, V13, P397

[10]

Xu W. T., 2012, J INT JOURAL APPL MA, V4, P460

← 1 2 →