Volume 7, Issue 3, June 2014, Pages 418 - 431
α-Quasi-Lock Semantic Resolution Method Based on Lattice-Valued Logic
Xiaomei Zhong, Yang Xu, Jun Liu, Shuwei Chen
Received 18 April 2012, Accepted 30 April 2012, Available Online 1 June 2014.
- https://doi.org/10.1080/18756891.2013.859868How to use a DOI?
- α-Quasi-lock semantic resolution method, resolution-based automated reasoning, general form of α-resolution principle, lattice-valued logic, lattice implication algebra
- 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.
- Open Access
- This is an open access article distributed under the CC BY-NC license.
Cite this article
TY - JOUR AU - Xiaomei Zhong AU - Yang Xu AU - Jun Liu AU - Shuwei Chen PY - 2014 DA - 2014/06 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 - https://doi.org/10.1080/18756891.2013.859868 ID - Zhong2014 ER -