![Sample our Computer Science journals, sign in here to start your access, latest two full volumes FREE to you for 14 days]({"type":"image" , "src" : "/sda/5928/TOC-Subject-Sample-2021-Computer-Science.jpg"})
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.