α -Paramodulation method for a lattice-valued logic L
            nF(X) with equality

Xingxing He; Yang Xu; J. Liu; Yingfang Li

doi:10.1007/s00500-020-05136-8

α -Paramodulation method for a lattice-valued logic L _nF(X) with equality

Xingxing He, Yang Xu, J. Liu, Yingfang Li

Research output: Contribution to journal › Article › peer-review

88 Downloads (Pure)

Abstract

In this paper, α-paramodulation and α-GH paramodulation methods are proposed for handling logical formulae with equality in a lattice-valued logic L _nF(X) , which has unique ability for representing and reasoning uncertain information from a logical point of view. As an extension of the work of He et al. (in: 2015 10th international conference on intelligent systems and knowledge engineering (ISKE), pp 18–20. IEEE, 2015; Uncertainty modelling in knowledge engineering and decision making: proceedings of the 12th international FLINS conference, pp 477–482. World Scientific, 2016), a new form of α-equality axioms set is proposed. The equivalence between α-equality axioms set and E _α-interpretation in L _nF(X) with an appropriate level is also established, which may provide a key foundation for equality reasoning in lattice-valued logic. Based on its equivalence, E _α-unsatisfiability equivalent transformation is given. Furthermore, α-paramodulation and its restricted method (i.e., α-GH paramodulation) are given. The soundness and completeness of the proposed methods are also examined.

Original language	English
Pages (from-to)	251-261
Journal	Soft Computing
Volume	25
Issue number	1
Early online date	15 Jul 2020
DOIs	https://doi.org/10.1007/s00500-020-05136-8
Publication status	Published (in print/issue) - 15 Jul 2020

Bibliographical note

Funding Information:
This research is supported by the National Natural Science Foundation of China (Grant Nos. 61603307, 61673320 and 61473239), the Grant from MOE (Ministry of Education in China) Project of Humanities and Social Sciences (Grant No. 19YJCZH048, 20XJCZH016), the Fundamental Research Funds for the Central Universities (Grant No. JBK2003006), and the Science and Technology Support Project of Sichuan province (Grant No. 2020YFG0045 and 2020YFG0238).

Publisher Copyright:
© 2020, Springer-Verlag GmbH Germany, part of Springer Nature.

Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.

Keywords

Equality
Lattice-valued logic
α-Equality axioms
α-GH paramodulation
α-Paramodulation

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/s00500-020-05136-8

SOCO_Accepted_VersionAuthor Accepted Manuscript, 173 KB

Cite this

@article{cf1d386aed1849cfa2356cd58ab85b45,

title = "α -Paramodulation method for a lattice-valued logic L nF(X) with equality",

abstract = "In this paper, α-paramodulation and α-GH paramodulation methods are proposed for handling logical formulae with equality in a lattice-valued logic L nF(X) , which has unique ability for representing and reasoning uncertain information from a logical point of view. As an extension of the work of He et al. (in: 2015 10th international conference on intelligent systems and knowledge engineering (ISKE), pp 18–20. IEEE, 2015; Uncertainty modelling in knowledge engineering and decision making: proceedings of the 12th international FLINS conference, pp 477–482. World Scientific, 2016), a new form of α-equality axioms set is proposed. The equivalence between α-equality axioms set and E α-interpretation in L nF(X) with an appropriate level is also established, which may provide a key foundation for equality reasoning in lattice-valued logic. Based on its equivalence, E α-unsatisfiability equivalent transformation is given. Furthermore, α-paramodulation and its restricted method (i.e., α-GH paramodulation) are given. The soundness and completeness of the proposed methods are also examined. ",

keywords = "Equality, Lattice-valued logic, α-Equality axioms, α-GH paramodulation, α-Paramodulation",

author = "Xingxing He and Yang Xu and J. Liu and Yingfang Li",

note = "Funding Information: This research is supported by the National Natural Science Foundation of China (Grant Nos. 61603307, 61673320 and 61473239), the Grant from MOE (Ministry of Education in China) Project of Humanities and Social Sciences (Grant No. 19YJCZH048, 20XJCZH016), the Fundamental Research Funds for the Central Universities (Grant No. JBK2003006), and the Science and Technology Support Project of Sichuan province (Grant No. 2020YFG0045 and 2020YFG0238). Publisher Copyright: {\textcopyright} 2020, Springer-Verlag GmbH Germany, part of Springer Nature. Copyright: Copyright 2020 Elsevier B.V., All rights reserved.",

year = "2020",

month = jul,

day = "15",

doi = "10.1007/s00500-020-05136-8",

language = "English",

volume = "25",

pages = "251--261",

journal = "Soft Computing",

issn = "1432-7643",

publisher = "Springer",

number = "1",

}

TY - JOUR

T1 - α -Paramodulation method for a lattice-valued logic L nF(X) with equality

AU - He, Xingxing

AU - Xu, Yang

AU - Liu, J.

AU - Li, Yingfang

N1 - Funding Information: This research is supported by the National Natural Science Foundation of China (Grant Nos. 61603307, 61673320 and 61473239), the Grant from MOE (Ministry of Education in China) Project of Humanities and Social Sciences (Grant No. 19YJCZH048, 20XJCZH016), the Fundamental Research Funds for the Central Universities (Grant No. JBK2003006), and the Science and Technology Support Project of Sichuan province (Grant No. 2020YFG0045 and 2020YFG0238). Publisher Copyright: © 2020, Springer-Verlag GmbH Germany, part of Springer Nature. Copyright: Copyright 2020 Elsevier B.V., All rights reserved.

PY - 2020/7/15

Y1 - 2020/7/15

N2 - In this paper, α-paramodulation and α-GH paramodulation methods are proposed for handling logical formulae with equality in a lattice-valued logic L nF(X) , which has unique ability for representing and reasoning uncertain information from a logical point of view. As an extension of the work of He et al. (in: 2015 10th international conference on intelligent systems and knowledge engineering (ISKE), pp 18–20. IEEE, 2015; Uncertainty modelling in knowledge engineering and decision making: proceedings of the 12th international FLINS conference, pp 477–482. World Scientific, 2016), a new form of α-equality axioms set is proposed. The equivalence between α-equality axioms set and E α-interpretation in L nF(X) with an appropriate level is also established, which may provide a key foundation for equality reasoning in lattice-valued logic. Based on its equivalence, E α-unsatisfiability equivalent transformation is given. Furthermore, α-paramodulation and its restricted method (i.e., α-GH paramodulation) are given. The soundness and completeness of the proposed methods are also examined.

AB - In this paper, α-paramodulation and α-GH paramodulation methods are proposed for handling logical formulae with equality in a lattice-valued logic L nF(X) , which has unique ability for representing and reasoning uncertain information from a logical point of view. As an extension of the work of He et al. (in: 2015 10th international conference on intelligent systems and knowledge engineering (ISKE), pp 18–20. IEEE, 2015; Uncertainty modelling in knowledge engineering and decision making: proceedings of the 12th international FLINS conference, pp 477–482. World Scientific, 2016), a new form of α-equality axioms set is proposed. The equivalence between α-equality axioms set and E α-interpretation in L nF(X) with an appropriate level is also established, which may provide a key foundation for equality reasoning in lattice-valued logic. Based on its equivalence, E α-unsatisfiability equivalent transformation is given. Furthermore, α-paramodulation and its restricted method (i.e., α-GH paramodulation) are given. The soundness and completeness of the proposed methods are also examined.

KW - Equality

KW - Lattice-valued logic

KW - α-Equality axioms

KW - α-GH paramodulation

KW - α-Paramodulation

UR - http://www.scopus.com/inward/record.url?scp=85087929691&partnerID=8YFLogxK

U2 - 10.1007/s00500-020-05136-8

DO - 10.1007/s00500-020-05136-8

M3 - Article

AN - SCOPUS:85087929691

SN - 1432-7643

VL - 25

SP - 251

EP - 261

JO - Soft Computing

JF - Soft Computing

IS - 1

ER -