α-Minimal Resolution Principle For A Lattice-Valued Logic

DOI

10.2991/ijcis.2015.8.1.3How to use a DOI?

Keywords

Automated reasoning, lattice-valued propositional logic LP(X), lattice-valued first-order logic LF(X), α-minimal resolution principle, α-minimal resolution group

Abstract

Based on the academic ideas of resolution-based automated reasoning and the previously established research work on binary α-resolution based automated reasoning schemes in the framework of lattice-valued logic with truth-values in a lattice algebraic structure-lattice implication algebra (LIA), this paper is focused on investigating α-n(t)-ary resolution based dynamic automated reasoning system based on lattice-valued logic based in LIA. One of key issues for α-n(t)-ary resolution dynamic automated reasoning is how to choose generalized literals in each resolution. In this paper, the definition of α-minimal resolution principle which determines how to choose generalized literals in LP(X) is introduced firstly, as well as its soundness and completeness being proved. α-minimal resolution principle is then further established in the corresponding lattice-valued first-order logic LF(X) along with its soundness theorem, lifting lemma and completeness theorem. These results lay the theoretical foundation for research of α-n(t)-ary resolution dynamic automated reasoning.

Copyright

© 2017, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - JOUR
AU  - Hairui Jia
AU  - Yang Xu
AU  - Yi Liu
AU  - Jun Liu
PY  - 2015
DA  - 2015/01/01
TI  - α-Minimal Resolution Principle For A Lattice-Valued Logic
JO  - International Journal of Computational Intelligence Systems
SP  - 34
EP  - 43
VL  - 8
IS  - 1
SN  - 1875-6883
UR  - https://doi.org/10.2991/ijcis.2015.8.1.3
DO  - 10.2991/ijcis.2015.8.1.3
ID  - Jia2015
ER  -