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.
Bibliographical noteFunding 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).
© 2020, Springer-Verlag GmbH Germany, part of Springer Nature.
Copyright 2020 Elsevier B.V., All rights reserved.
- Lattice-valued logic
- α-Equality axioms
- α-GH paramodulation