α-Quasi-Lock Semantic Resolution Method Based on Lattice-Valued Logic

DOI

10.1080/18756891.2013.859868How to use a DOI?

Keywords

α-Quasi-lock semantic resolution method, resolution-based automated reasoning, general form of α-resolution principle, lattice-valued logic, lattice implication algebra

Abstract

Based on the general form of α-resolution principle for a lattice-valued logic with truth-values defined in a lattice-valued logical algebra structure - lattice implication algebra, the further extended α-resolution method in this lattice-valued logic is discussed in the present paper in order to increase the efficiency of the resolution method. Firstly, α-quasi-lock semantic resolution method in lattice-valued propositional logic LP(X) is established by combining the lock and semantic resolution simultaneously, and its theorems of soundness and conditional completeness are proved. Secondly, this α-quasi-lock semantic resolution method is extended into the corresponding lattice-valued first-order logic LF(X), and its soundness and conditional completeness are also established. This extended resolution method will provide a theoretical basis for automated soft theorem proving and program verification based on lattice-valued logic.

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  - Xiaomei Zhong
AU  - Yang Xu
AU  - Jun Liu
AU  - Shuwei Chen
PY  - 2014
DA  - 2014/06/01
TI  - α-Quasi-Lock Semantic Resolution Method Based on Lattice-Valued Logic
JO  - International Journal of Computational Intelligence Systems
SP  - 418
EP  - 431
VL  - 7
IS  - 3
SN  - 1875-6883
UR  - https://doi.org/10.1080/18756891.2013.859868
DO  - 10.1080/18756891.2013.859868
ID  - Zhong2014
ER  -