Multi-ary α-semantic resolution automated reasoning based on lattice-valued first-order logic LF ( X ) 1

Abstract

This paper focuses on multi-ary α-semantic resolution automated reasoning method based on multi-ary α-resolution principle for a lattice-valued logic with truth-value in a lattice implication algebra. Firstly, the definitions of the multi-ary α-semantic resolution and multi-ary α-semantic resolution deduction in LF (X) are given, respectively, the soundness and completeness of this ground case are gotten. Secondly, the validity of multi-ary α-semantic resolution method is analyzed. Thirdly, the algorithm for multi-ary α-semantic resolution methods based on lattice-valued first-order logic LF (X) is constructed. This work will provide a theoretical foundation for the more efficient resolution based automated reasoning in lattice-valued logic.

Keywords

Incomparability lattice implication algebra lattice-valued logic automated reasoning multi-ary α-semantic resolution multi-ary α-semantic resolution deduction and soundness completeness

1 Introduction

Resolution was introduced by Robinson in his landmark paper [9] in 1965 as a merchanizable method for detecting the unsatisfiability of a given set of formulae in classical first-order logic, it revolutionized the field of automated reasoning, and since then, many refinements of resolution have been proposed by researchers to cut down the search space and increase efficiency. One of the most important refinements of resolution is semantic resolution [11] which was introduced by Slagle in 1967. In semantic resolution method, it utilize the technology that restraining the type of clauses and the order of literals participated in resolution procedure to reduce the redundant clauses, and can increase the efficiency of reasoning, the order of predicate symbol in semantic resolution is a coarse order, because there can exist more than one predicate symbols in one clause in first-order logic, among these identical predicate symbols, there are no order, so the resolution literals can not be selected solely. In order to select the resolution literals solely in resolution procedure and reduce the new clause, in 1971, Reiter.R presented the ordered clause semantic resolution–OI-resolution [10], the efficiency of OI-resolution is very high in many cases. Unfortunately, it is incomplete. In 1979, Liu applies the idea of indexing the literals in lock resolution method presented by Boyer, and introduced a new semantic resolution method–IDI-resolution [2], IDI-resolution possess the advantages of PI-resolution and OI-resolution, and it is complete for clause set in first-order logic. Subsequently, Liu, Lu etc. investigated various kinds of resolution methods [1 –5], Liu [5] studied the relation among the linear resolution, semantic resolution and lock resolution.

As the use of non-classical logics becomes increasingly important in computer science, AI and logic programming, the developing efficient automated theorem proving based on non-classical logic is also an active area of research (e.g., for fuzzy logic and many-valued logic, among others. The essential idea in many of those methods is to transform the resolution algorithm in fuzzy logic and many-valued logic to that of classical logic. As far as we know, proof theory for lattice-valued logic has so far not been extensively developed. There have also been investigations of resolution-based automated reasoning in lattice-valued logic based on LIAs (e.g., among others, [16 –26]. The aim of dealing with incomparability leads to the complexity of logical formula in LIAs based lattice-valued logic. With the development of research, it shows that 2-ary α-resolution automated reasoning based on lattice-valued logic aiming at processing uncertain information with incomparability is scientific and effective. But there are two aspects limitations in 2-ary α-resolution automated reasoning: (1) 2-ary α-resolution can only process the resolution of 2-ary generalized literals; (2) the number of resolution generalized literals is fixed at 2 in each resolution in 2-ary α-resolution deduction. The limitations of these two aspects makes the 2-ary α-resolution automated reasoning theory and applications are limited, and also directly affect the efficiency of 2-ary α-resolution automated reasoning. The complexity of lattice-valued logic systems based on LIAs and the logical formulae, will limit the efficiency of 2-ary α-resolution automated reasoning. Therefore, it is necessary to study resolution automated reasoning theory, methods, algorithms and procedures which improving the resolution automated reasoning efficiency under the premise of keeping the depict ability in complexity problems. To resolve these limitations, Xu [21] extend the 2-ary α-resolution in this lattice-valued logic into a more general form, i.e., from 2-ary α-resolution to multi-ary α-resolution, the multi-ary α-resolution principle in lattice-valued propositional logic LP (X) and lattice-valued first-order logic LF (X), respectively. And its theorems of both soundness and completeness are proved in LP (X). In the corresponding lattice-valued first-order logic LF (X), the soundness theorem, lifting lemma and completeness theorem of multi-ary α-resolution principle are also established. These works will place a theoretical support for establishing automated reasoning algorithm and its implementation with further applications into automated deduction and decision making problem under uncertainty.

The current work is organized as follows: In Section 2, we mainly list some basic concepts and some properties of lattice implication algebras, lattice-valued propositional logic and lattice valued first-order logic, they will be used in other sections; In Section 3, we mainly investigate the descent lemma and equivalent transform theorem of multi-ary α-resolution methods in LF (X); In section 4, we mainly investigate the multi-ary α-semantic resolution automated reasoning method based on LF (X) with truth-value in a lattice implication algebra, gives the soundness and completeness theorems on this resolution method; In Section 5, we analysis the validity of multi-ary α-semantic resolution method in lattice-valued first-order logic LF (X) from four aspects; In Section 6, we construct the algorithm for multi-ary α-semantic resolution methods based on lattice-valued first-order logic LF (X), the completeness and soundness of this algorithm will be studied. This work will provide a theoretical foundation for the more efficient resolution based automated reasoning in lattice-valued logic.

2 Preliminaries

In the following, we will introduce some elementary concepts and conclusions of lattice-valued logic with truth-value in a lattice implication algebra. We refer the readers to [18] for more details.

2.1 Lattice implication algebras

Definition 2.1. [13] Let (L, ∨ , ∧ , O, I) be a bounded lattice with an order-reversing involution ^′, the greatest element I and the smallest element O, and

$\to : L \times L ⟶ L$ be a mapping. $L = (L, \lor, \land,^{'}, \to, O, I)$ is called a lattice implication algebra if the following conditions hold for any x, y, z ∈ L:

(I₁) x → (y → z) = y → (x → z);

(I₂) x → x = I;

(I₃)x → y = y′ → x′;

(I₄) x → y = y → x = I implies x = y;

(I₅) (x → y) → y = (y → x) → x;

(l₁) (x ∨ y) → z = (x → z) ∧ (y → z);

(l₂) (x ∧ y) → z = (x → z) ∨ (y → z).

In this paper, we denote $L$ as a lattice implication algebra (L, ∨ , ∧ , ′, → , O, I).

Example 2.1. Let L = {O, a, b, c, d, I}, the Hasse diagram of L be defined as Fig. 1 and its implication operator → be defined as Table 1 and operator ^′ be defined as Table 2. Then L = (L, ∨ , ∧ , ′, → , O, I) is a lattice implication algebra.

Example 2.2. (Lukasiewicz implication algebra on a finite chain) Let L _n = {a _i|i = 1, 2, ⋯ , n} , a ₁ ≤ a₂ ≤ ⋯ a _n. For any 1 ≤ j, k ≤ n, define

$\begin{matrix} a_{j} \lor a_{k} & = & a_{\max {j, k}}, a_{j} \land a_{k} = a_{\min {j, k}}, \\ (a_{j})^{'} & = & a_{n - j + 1}, a_{j} \to a_{k} = a_{\min {n - j + k, n}} . \end{matrix}$

Then (L _n, ∨ , ∧ , ′, → , a ₁, a _n) is a lattice implication algebra.

2.2 Multi-ary α-resolution principle based on lattice-valued propositional logic LP (X)

Definition 2.2. [6] Let X be a set of propositional variables, T = L ∪ {′, →} be a type with ar(^′)=1, ar(→)=2 and ar(α)=0 for any α ∈ L. The propositional algebra of the lattice-valued propositional calculus on the set X of propositional variables is the free T-algebra on X is denoted by LP (X).

Theorem 2.2. [8] LP (X) is the minimal set Y which satisfies:

X ∪ L ⊆ Y .

if p, q ∈ Y, then p′, p → q ∈ Y .

Definition 2.3. [6, 14] A valuation of LP (X) is a propositional algebra homomorphism v : LP (X) → L.

Definition 2.4. [13] Let p ∈ LP (X) , α ∈ L, If there exists a valuation v of LP (X) such that v (p) ≰ α, p is satisfiable by a truth-value level α, in short,α-satisfiable; If v (p) ≰ α for every valuation v, p is valid at the truth-value level α, in short, α-valid. If α = I, then p is valid simply.

Definition 2.5. [18] Let p ∈ LP (X). If v (p) ≤ α for any valuation v of LP (X), p is always false at the truth-valued level α, in short, α-false. If α = O, then p is false.

Definition 2.6. [18] A lattice-valued propositional logical formula f is called an extremely simple form (in short, ESF), if a lattice-valued propositional logical formula f ^* obtained by deleting any constant or literal or implication item appearing in f is not equivalent to f.

Definition 2.7. [18] A lattice-valued propositional logical formula f is called an indecomposable extremely simple form (in short, IESF), if:

(1) f is an ESF containing connective → and ^′.

(2) for any g ∈ LP (X), if $g \in \bar{f}$ in $\bar{LP (X)}$ , then g is an ESF containing connective → and ^′ at most, where

$\bar{LP (X)} = (LP (X) /_{=}, \lor, \land,^{'}, \to)$ is a lattice implication algebra.

$LP (X) /_{=} = {\bar{p} | p \in LP (X)}, \bar{p} = {q \in LP (X) | q$ = p} .

Definition 2.8. [18] All the constants, literals and IESFs are generalized literals.

Definition 2.9. [21] (Multi-ary α-Resolution Principle) Let C _i = p _i1 ∨ ⋯ ∨ p _{i
_{m
_i}} be generalized clauses of LP (X), H _i = {p _i1, ⋯ , p _{i
_{m
_i}}} the set of all disjuncts occurring in C _i, i = 1, 2, ⋯ , m, α ∈ L. For any i ∈ {1, 2, ⋯ , m}, if there exist generalized literals x _i ∈ H _i such that x ₁ ∧ x ₂ ∧ ⋯ ∧ x _m ≤ α, then C ₁ (x ₁ = α) ∨ C ₂ (x ₂ = α) ∨ ⋯ ∨ C _m (x _m = α) is called an m-ary α-resolvent of C ₁, C ₂, ⋯ , C _m, denoted by R _p(m-α) (C ₁ (x ₁) , C ₂ (x ₂) , ⋯ , C _m (x _m)) , x ₁, x ₂, ⋯ , x _m are called an m-ary α-resolution group. The m-ary α-resolution group x ₁, x ₂, ⋯ , x _m, denoted by (x ₁, x ₂, ⋯ , x _m) - α.

Theorem 2.3. [21] (Soundness) SupposeS = C ₁ ∧ C ₂ ∧ ⋯ C _m, where C ₁, C ₂, ⋯ , C _m are generalized clauses in LP (X). {Φ ₁, Φ ₂, ⋯ , Φ _t} is a multi-ary α-resolution deduction from S to Φ _t. If Φ _t ≤ α, then S ≤ α.

Theorem 2.4. [21] (completeness) Suppose S = C ₁ ∧ C ₂ ∧ ⋯ C _m, where C ₁, C ₂, ⋯ , C _m are generalized clauses in LP (X). If S ≤ α, then there exists a multi-ary α-resolution deduction from S to α-empty clause.

2.3 Multi-ary α-resolution principle based on lattice-valued first-order logic LF (X)

Definition 2.10. [7, 15] Suppose V and F are the set of variable symbols and that of functional symbols in LF (X), respectively, the set of terms of LF (X) is defined as the smallest set J satisfying the following conditions:

V ⊆ J;

For any n ∈ N, if f ⁽ⁿ⁾ ∈ F, then for any t ₁, ⋯ , t _n ∈ J, f ⁽ⁿ⁾ (t ₁, ⋯ , t _n) ∈ J.

Remark 2.1. f ⁽⁰⁾ is specified as a constant symbol.

Definition 2.11. [18] Suppose P is a predicate symbol set in LF (X). The set of atoms of LF (X) is defined as the smallest set A _t satisfying the following condition: For any n ∈ N, if P ⁽ⁿ⁾ ∈ P, then P ⁽ⁿ⁾ (t ₀, t ₁, ⋯ , t _n) ∈ A _t for any t ₀, t ₁, ⋯ , t _n ∈ J.

Definition 2.12. [14] The set of formulas of LF (X) is defined as the smallest set F satisfying the following conditions:

A _t ⊂ F;

If p, q ∈ F, then p → q ∈ F;

If p ∈ F and x is a free variable in p, then (∀ x) p, (∃ x) p ∈ F.

Definition 2.13. [18] Suppose G ∈ F, F _G is the set of all functional symbols occurring in G, P _G is the set of all predicate symbols occurring in G, and D(& ∅) is the domain of interpretations. An interpretation of G over D is a triple I _D = 〈D, μ _D, v _D〉, where,

$\begin{matrix} μ_{D} : & F_{G} \to U_{D} = {f_{D}^{(n)} : D^{n} \to D | n \in N} \\ f^{0} \mapsto f_{D}^{0}, f_{D}^{0} (D^{0}) = {f_{D}^{0}} \subseteq D, D^{0} ≠ \emptyset \\ f^{n} \mapsto f_{D}^{n} (n \in N^{+}) . \\ v_{D} : & P_{G} \to V_{D} = {p_{D}^{(n)} : D^{n} \to L | n \in N} \\ p^{0} \mapsto p_{D}^{0}, p_{D}^{0} (D^{0}) = {p_{D}^{0}} \subseteq D, \\ p^{n} \mapsto p_{D}^{n} (n \in N^{+}) . \end{matrix}$

Definition 2.14. [18] A formula G in lattice-valued first-order logic LF (X) is a generalized-literal, if it satisfies the following conditions:

G is a literal; or

G is constructed only by some literals and some implication connectives with the condition that G cannot be represented by connectives ∨ or ∧ and G cannot be decomposed into a simpler form (G is called an indecomposable implication form).

Definition 2.15. [18] Let G ∈ F,α ∈ L. G is said to be α-false, if v _D (G) ≤ α for any interpretation I _D = 〈D, μ _D, v _D〉 of G.

Definition 2.16. [18] Suppose G is a formula of the form Q ₁ x ₁ ⋯ Q _n x _n G ^*, where Q ₁, ⋯ , Q _n are the quantifiers, i.e.,∀ or ∃, and G ^* is a formula without any quantifier. Then G is said to be a generalized-prenex conjunctive normal form, if G ^* is a generalized-conjunctive normal form.

Definition 2.17. [7] Suppose a formula

$G = Q_{1} x_{1} \dots Q_{n} x_{n} M$ is a generalized-prenex conjunctive normal form. The formula G ^* obtained by the following steps is called a generalized-Sk $\ddot{o}$ lem standard form of G:

If Q _r is an existential quantifier and without any universal quantifier occurring ahead it in the prefix Q ₁, ⋯ , Q _n (from left to right), we choose a new constant c different from other constants occurring in M, replace all x _r occurring in M by c, and then delete Q _r from the prefix Q ₁, ⋯ , Q _n.

If Q _r is an existential quantifier and Q _k1, ⋯ , Q _km are all the universal quantifiers occurring ahead Q _r (m ≥ 1, 1 ≤ k1 < ⋯ < km < r), we choose a new m-ary function symbol f ^(m) different from all other function symbols occurring in M, replace all x _r in M by f ^(m) (x _k1, ⋯ , x _km) and then delete Q _r from the prefix Q ₁, ⋯ , Q _n.

Repeating (1) and (2) until there is no existential quantifier occurring in the prefix.

Definition 2.18. [21] (Multi-ary α-Resolution Principle) Let C _i = p _i1 ∨ ⋯ ∨ p _{i
_{m
_i}} be generalized clauses of LF (X), H _i = {p _i1, ⋯ , p _{i
_{m
_i}}} the set of all disjuncts occurring in C _i, i = 1, 2, ⋯ , m, α ∈ L. For any i ∈ {1, 2, ⋯ , m}, if there exist generalized literals x _i ∈ H _i and a substitution σ such that $x_{1}^{σ} \land x_{2}^{σ} \land \dots \land x_{m}^{σ} & # x 2264; α$ , then

$C_{1}^{σ} (x_{1}^{σ} = α) \lor C_{2}^{σ} (x_{2}^{σ} = α) \lor \dots \lor C_{m}^{σ} (x_{m}^{σ} = α)$ is called an m-ary α-resolvent of C ₁, C ₂, ⋯ , C _m, denoted by

$R_{f (m - α)} (C_{1} (x_{1}), C_{2} (x_{2}), \dots, C_{m} (x_{m})) .$ x ₁, x ₂, ⋯ , x _m are called an m-ary α-resolution group.

Theorem 2.5. [21] (Soundness) Suppose S = C₁ ∧ C₂ ∧ ⋯ C_m, where C₁, C₂, ⋯ , C_m are generalized clauses in LF (X). {Φ₁, Φ₂, ⋯ , Φ_t} is a multi-ary α-resolution deduction from S to Φ_t. If Φ_t ≤ α, then S ≤ α.

Theorem 2.6. [21] (completeness) Suppose S = C₁ ∧ C₂ ∧ ⋯ C_m, where C₁, C₂, ⋯ , C_m are generalized clauses in LF (X). If S ≤ α, then there exists a multi-ary α-resolution deduction from S to α-empty clause.

In this paper, the definitions of substitution, the most general unifier, ground substitution, instance, ground instance used below are all defined in the same way as those in classical logic. In addition, α is assumed to be always less than I.

3 Descent lemma and equivalent transform theorem of multi-ary α-resolution in LF (X)

Definition 3.1 [21] (H-interpretation) Suppose G ^* is a generalized sk $\ddot{o}$ lem standard form of a formula G, H is the H-field of G ^*, $I_{H} = 〈 H, u_{H}, v_{H} 〉$ is an interpretation of G ^* over H. $I_{H}$ is said to be an H-interpretation of G ^*, if

$\begin{matrix} u_{H} : & F_{G^{*}} \to U_{H} = {f_{H}^{n} : H^{n} \to H | n \in N}, \\ f^{(0)} \to f_{H}^{(0)}, (f_{H}^{(0)} (H^{0}) = {f^{0}} \subseteq H_{0}), \\ (where H^{0} = H_{0}) \\ f^{(n)} \to f_{H}^{(n)}, \\ f_{H}^{(n)} (h_{1}, h_{2}, \dots, h_{n}) = f^{(n)} (h_{1}, h_{2}, \dots, h_{n}) \\ (where n \in N^{+}) \\ v_{H} : & P_{G^{*}} \to V_{H} = {p_{H}^{(n)} : H^{n} \to L | n \in N}, \\ p^{(0) \to p_{H}^{(0)}}, (p_{H}^{(0)} (H^{0}) = {p^{0}} \subseteq L, H^{0} = H_{0}) \\ p^{(n)} \to p_{H}^{(n)}, (n \in N^{+}) \end{matrix}$

Theorem 3.1. [21] Let G ^* is a generalized-Skölem standard form of a formula G, and |L| < ℵ ₀. G ^* is α-false if and only if there exists a finite ground instance set G ^*0 of G ^* such that $G_{c}^{* 0}$ is α-false, where $G_{c}^{* 0}$ is the conjunction of all ground instances of G ^*0.

Theorem 3.2. Let α ∈ L, G₁, G₂, ⋯ , G_m are generalized literals in lattice-valued first-order logicLF (X), g₁, g₂, ⋯ , g_m are generalized literals inlattice-valued propositional logic LP (X) such thatg₁, g₂, ⋯ , g_m are ground instances of G₁, G₂, ⋯ , G_m, respectively. Then g₁, g₂, ⋯ , g_m is an m-ary resolution group in LP (X) if and only if G₁, G₂, ⋯ , G_m is also an m-ary resolution group in LF (X).

Proof. Necessity is directly from the lifting lemma of multi-ary α-resolution principle. Now, we need to prove its sufficiency.

Assume that G ₁, G ₂, ⋯ , G _m is m-ary resolution group in LF (X), then we have v _D (G ₁ ∧ G ₂ ∧ ⋯ ∧ G _m) ≤ α for any interpretation I _D = 〈D, u _D, v _D〉. If there is some common variables in G ₁, G ₂, ⋯ , G _m, then we can make a rename subsititute for G ₁, G ₂, ⋯ , G _m such that there is no common variables in G _i (i = 1, 2, ⋯ , m). Therefore, loss generality, we can assume that there is no common variables in G _i (i = 1, 2, ⋯ , m). Let g _i be ground instance of G _i (i = 1, 2, ⋯ , m), respectively. For any valuation function v _H of g ₁, g ₂, ⋯ , g _m in LP (X), there exist H-interpretation on v _H such that v _H (g ₁ ∧ g ₂ ∧ ⋯ ∧ g _m) = v _D (G ₁ ∧ G ₂ ∧ ⋯ ∧ G _m) ≤ α . Therefore g ₁, g ₂, ⋯ , g _m is an m-ary resolution group in LP (X).

Remark 3.1. Theorem 3.2 is called Descent Lemma of multi-ary α-resolution in lattice-valued first-order logic LF (X).

Theorem 3.3. Let S be a generalized clause set in lattice-valued first-order logic LF (X) and α ∈ L. There exist a multi-ary α-resolution deduction w = {Φ ₁, Φ ₂, ⋯ , Φ _t} from S to Φ _t in LF (X) if and only if there exist a multi-ary α-resolution deduction $w^{0} = {Φ_{1}^{0}, Φ_{2}^{0}, \dots, Φ_{t}^{0}}$ from S ⁰ to $Φ_{t}^{0}$ in LP (X), where the generalized clause of S ⁰ and $Φ_{i}^{0}$ are the ground instances of generalized clause of S and Φ _i, respectively (i = 1, 2, ⋯ , t).

Proof. Sufficiency is directly from the lifting lemma of multi-ary α-resolution principle. Now, we need to prove its necessity. By the generalized literals in S0 are all ground instance of corresponding generalized literals in S, for each α-resolvent $Φ_{i} (i = 1, 2,, t)$ , there exist generalized clauses $C_{1}, C_{2},, C_{m}$ such that

$Φ_{i} = R_{f (m α)} (C_{1} (x_{1})), (C_{2} (x_{2})), (C_{m} (x_{m})),$

where $x_{1}, x_{2},, x_{m}$ are generalized literals in $C_{1}, C_{2},, C_{m}$ respectively, and there exists a substitution σ such that

$x_{1}^{σ} x_{2}^{σ} x_{m}^{σ} α .$

Therefore, for any interpretation $I_{D} = D, μ_{D}, v_{D}$ ,we have

$v_{D} (x_{1}^{σ} x_{2}^{σ} x_{m}^{σ}) α .$

As $x_{1}^{0} x_{2}^{0} x_{m}^{0}$ are ground instance of $x_{1}, x_{2},, x_{m}$ , respectively, for any valuation function $x_{1}^{0} x_{2}^{0} x_{m}^{0}$ in LP(X), there exits an H-interpretation I_H over v_H such that

$v_{H} (x_{1}^{0} x_{2}^{0} x_{m}^{0}) = v_{D} (x_{1}^{σ} x_{2}^{σ} x_{m}^{σ}) α$

Therefore,

$Φ_{1}^{0} = R_{p (m α)} (C_{1}^{0} (x_{1}^{0})), (C_{2}^{0} (x_{2}^{0})), (C_{m}^{0} (x_{m}^{0})),$

is the multi-ary α-resolvent of $C_{1}^{0}, C_{2}^{0},, C_{m}^{0}$ and $Φ_{i}^{0}$ is the ground instance of $Φ_{i}$ .

Remark 3.2 Theorem 3.3 is called Equivalent Transform Theorem between multi-ary α-resolution in lattice-valued first-order logic LF(X) and multi-ary α- resolution in lattice-valued propositional logic LF(X).

4 Multi-ary α-semantic resolution methods based on LF (X)

In this section, we suppose that generalized-clauses and generalized-literals always belong to a generalized-Sk $\ddot{o}$ lem standard form, i.e., for any generalized-clause C and generalized-literal g, all variables of C and g are bound variables with the quantifier ∀. For any generalized-clauses G ₁, G ₂, ⋯ , G _m (m ≥ 3), there always exists a renamed substitution such that G ₁, G ₂, ⋯ , G _m have no common variables. Therefore, we suppose that generalized-clauses G _i (i = 1, 2, ⋯ , m) discussed below have no common variables.

Definition 4.1. Let I _D = 〈D, μ _D, v _D〉 be an interpretation in lattice-valued first-order logic LF (X), α ∈ L. N, E ₁, ⋯ , E _q are generalized clauses sets in LF (X), $G$ is an order of generalized literals occurring in these clauses. The finite sequence (N, E ₁, E ₂, ⋯ , E _q) (*) where is called a multi-ary α-semantic clash w. r. t. I _D and $G$ , if (*) satisfy the following conditions:

For any generalized clause C ∈ E _i, v _D (C) ≤ α, i = 1, 2, ⋯ q;

Let R ₀ = ∨ _{N_j∈N} (N _j), for any i = 1, 2, ⋯ , q, there exists a multi-ary α-resolution formula R _i of N _i and E _i, where N ₁ = N, $N_{i} = {R_{1}} \cup N_{2}^{*}$ , $N_{2}^{*} \subset N$ . For any i = 3, 4, ⋯ , q, $N_{i} = {R_{i - 1}} \cup N_{i}^{*}$ , $N_{i}^{*} \subset N \cup {R_{1}, R_{2}, \dots, R_{i - 2}}$ .

For any generalized clause C ∈ E _i, theα-resolution generalized literals in C is the leftmost generalized literals in C.

v _D (R _q) ≤ α.

R _q is called multi-ary α-sematic resolvent of this clash w. r. c. I _D and $G$ , N is called the core and E ₁, E ₂, ⋯ , E _q are called α-electrons group.

Remark 4.1. (1) In this Definition, for any generalized clause C, if the same disjunctive terms of C occurring in different places in C, then reserving the leftmost disjunction and deleting others.

(2) In this Definition, there exist C ∈ N such that C must be α-true, that is, v (C) ≰ α. In fact, if v (C) ≤ α for any C ∈ N, then v (R ₀) ≤ α, i.e., there is not a multi-ary α-semantic clash. If the R ₀ is regard as the multi-aryα-resolvent w. r. t. I _D and $G$ , then the multi-ary α-semantic resolvent w. r. t. I _D and $G$ will be redundancy.

(3) For any disjunctive term g in E _i(i = 1, 2, ⋯ , q), v (g) ≤ α.

Example 4.1. Let , C ₂ = (M (b) → N (y ₁)) ∨ P (y ₂), C ₃ = (Q (z ₁)→ be three generalized clauses in lattice-valued first logic L ₉ F (X), wherex ₁, x ₂, x ₃, y ₁, y ₂, z ₁, z ₂, z ₃ are variables and b, c are constants. Let α = a ₅, I _D = 〈D, μ _D, v _D〉 be aninterpretation in L ₉ F (x) and $G : (Q (z_{1}) \to P (c))^{'},$ be an order of generalized literals in these clauses, where D = {b, c},

$\begin{matrix} \frac{b}{b}, \frac{c}{c}, \frac{M (b)}{a_{7}}, \frac{M (c)}{a_{7}}, \frac{N (b)}{I}, \frac{N (c)}{I}, \frac{P (b)}{a_{3}}, \\ \frac{P (c)}{I}, \frac{Q (b)}{a_{7}}, \frac{Q (c)}{a_{3}}, \frac{R (b)}{a_{4}}, \frac{R (c)}{a_{4}} . \end{matrix}$

Under the interpretation I _D, v _D (C ₁) < α, v _D (C ₂) > α, v _D (C ₃) < α. There is a multi-ary α-semantic clash. In fact, the multi-ary α-semantic clash is (N, E ₁, E ₂), where N = {C ₂}, E ₁ = {C ₃}, E ₂ = {C ₁}. The multi-ary α-semantic resolvent is , where R ₀ = {C ₂} , R ₁ = (M (b) → N (y ₁)).

Theorem 4.1. Let N, E₁, E₂, ⋯ , E_q be generalized clause sets and I_D = 〈D, μ_D, v_D〉 be an interpretation in lattice-valued first-order logic LF (X), $G$ is an order of generalized literals occurring in these clauses. If the sequence (N, E₁, E₂, ⋯ , E_q) is a multi-aryα-semantic clash w. r. t. I_D and $G$ , R_q is a multi-ary α-semantic resolvent of this clash, then

$\land_{C \in N \cup E_{1} \cup E_{2} \cup \dots \cup E_{q}} C # x 2264; R_{q} .$

Proof. The proof is straightforward from [21].

Definition 4.2. Let S = C ₁ ∧ C ₂ ∧ ⋯ ∧ C _m, where C ₁, C ₂, ⋯ , C _m are generalized clauses in lattice-valued first-order logic LF (X), I _D be an interpretation in LF (X) and α ∈ L, $G$ is an order of generalized literals occurring in these clauses. A sequence: Φ ₁, Φ ₂, ⋯ , Φ _t is called a multi-ary α-semantic resolution deduction from S to Φ _t, if it satisfies the following conditions:

Φ _i ∈ {C ₁, C ₂, ⋯ , C _m} (i = 1, 2, ⋯ , t) or

Φ _i is a multi-ary α-semantic resolvent w. r. t. I _D and $G$ , where the core and electrons of Φ _i are composed of Φ _j (j < i) or generalized clauses occurring in S.

Theorem 4.2. Let S = C₁ ∧ C₂ ∧ ⋯ ∧ C_m, where C₁, C₂, ⋯ , C_m are generalized clauses in lattice-valued first-order logic LF (X), I_D be a valuation in LF (X) and α ∈ L, $G$ is an order of generalized literals occurring in these clauses. There exists a multi-ary α-semantic resolution deduction from S to Φ_t:Φ₁, Φ₂, ⋯ , Φ_t, and Φ_t is α-empty clause, then S ≤ α.

Proof. According to the soundness of the general form of α-resolution principle in lattice-valued first-order logic LF (X), we can obtain the result easily.

Theorem 4.3. (Lifting Lemma) Let N, E₁, E₂, ⋯ , E_q be generalized clause sets in lattice valued first-order logic LF (X) and I_{D
⁰} = 〈D⁰, μ_{D
⁰}, v_{D
⁰}〉 be an interpretation in LF (X), α ∈ L. $N^{0}, E_{i}^{0}$ are the sets of instance of generalized clause in N, E_i, respectively, where i = 1, 2, ⋯ , q. If $(N^{0}, E_{1}^{0}, E_{2}^{0}, \dots, E_{q}^{0})$ is a multi-ary α-semantic clash w. r. t. I_{D
⁰} and $G$ , $R_{q}^{0}$ is the multi-ary α-semantic resolvent of this clash, then there exit an interpretation in LF (X) such that is a multi-ary α-semantic clash and $R_{q}^{0}$ is an instance of R_q, where R_q is the multi-ary α-semantic resolvent of the clash (N, E₁, E₂, ⋯ , E_q), i. e., Fig. 2 holds.

Proof. For any generalized clauses C _i, C _j ∈ N ∪ E ₁ ∪ E ₂ ∪ ⋯ ∪ E _q, if C _i, C _j have common variables, then there exist rename transforms such that C _i, C _j have no common variables. Therefore, we can discussed only the situation that there have no common variables in any generalized clauses in N ∪ E ₁ ∪ E ₂ ∪ ⋯ ∪ E _q.

Let $N_{i}^{0}$ be any generalized clause in N and $E_{jh}^{0}$ be any generalized clause in E _j, then there exist substitution ɛ _i, ɛ _jh such that $N_{i}^{0} = N_{i}^{ɛ_{i}}, E_{jh}^{0} = E_{jh}^{ɛ_{jh}}$ , where N _i ∈ N and E _jh ∈ E _j, j = 1, 2, ⋯ , q. Let $ɛ = (\cup_{i \in Γ} ɛ_{i}) \cup (\cup_{j = 1}^{q} (\cup_{h \in Σ_{i}} ɛ_{jh}))$ , where Γ, Σ _i are index sets, then $N_{i}^{0} = N_{i}^{ɛ}, E_{jh}^{0} = E_{jh}^{ɛ}$ . Since $(N^{0}, E_{1}^{0}, E_{2}^{0}, \dots, E_{q}^{0})$ is a multi-ary α-semantic clash w. r. t. I _{D
⁰} and $G$ , then $v_{D^{0}} (E_{jh}^{0}) & # x 2264; α$ . For any j = 1, 2, ⋯ , q, let N = {N ₁, N ₂, ⋯ , N _k}, E _j = {E _j1, E _j2, ⋯ , E _jp}, then

$N^{0} = {N_{1}^{0}, N_{2}^{0}, \dots, N_{k}^{0}}, E_{j}^{0} = {E_{j 1}^{0}, E_{j 2}^{0}, \dots, E_{jp}^{0}},$ where $N_{i}^{0} = N^{ɛ}$ , $E_{jh}^{0} = E_{jh}^{ɛ}$ , i = 1, 2, ⋯ , k, h = 1, 2, ⋯ , p. Let $H_{i}^{0}$ be the set of all disjunctive terms occurring in $N_{i}^{0}$ and $H_{jh}^{0}$ be the set of all disjunctive terms occurring in $E_{jh}^{0}$ , where i = 1, 2, ⋯ , k, h = 1, 2, ⋯ , p, j = 1, 2, ⋯ , q. Since $(N^{0}, E_{1}^{0}, E_{2}^{0}, \dots, E_{q}^{0})$ is a multi-ary α-semantic clash w. r. t. I _{D
⁰} and $G$ , then there exist a substitution σ and $x_{i}^{0} \in H_{i}^{0}, y_{h}^{0} \in H_{jh}^{0} (i = 1, 2, \dots, k, h = 1, 2, \dots, p)$ such that $x_{1}^{0 σ} \land \dots \land x_{k}^{0 σ} \land y_{1}^{0 σ} \land \dots \land y_{p}^{0 σ} & # x 2264; α$ , where $v_{D^{0}} (x_{i}^{0 σ}) & # x 2270; α$ and $y_{h}^{0 σ}$ is the leftmost disjunctive term in $E_{jh}^{0 σ}$ , $x_{i}^{0} = x_{i}^{ɛ}, y_{h}^{0} = y_{h}^{ɛ}, i = 1, 2, \dots, k, h = 1, 2, \dots, p$ . Then the multi-ary α-semantic resolvent $R_{i}^{0}$ of N and $E_{j}^{0}$ is equal to $R_{i}^{0} = N_{1}^{0 σ} (x_{1}^{0 σ} = α) \lor N_{2}^{0 σ} (x_{2}^{0 σ} = α) \lor \dots \lor N_{k}^{0 σ} (x_{k}^{0 σ} = α) \lor E_{j 1}^{0 σ} (y_{1}^{0 σ} = α) \lor \dots E_{jp}^{0 σ} (y_{p}^{0 σ} = α) .$ By the choice of ɛ, we have $R_{i}^{0} = N_{1}^{0 σ ɛ} \lor N_{2}^{0 σ ɛ} \lor \dots \lor N_{k}^{0 σ ɛ} \lor E_{j 1}^{0 σ ɛ} \lor \dots E_{jp}^{0 σ ɛ} \lor α .$ According to the proof of Lifting Lemma of multi-ary α-resolution principle in LF(X), there exists a most general unifier λ such that ɛσ = λδ, where δ is a substitution. Since $x_{1}^{0 σ} \land \dots \land x_{k}^{0 σ} \land y_{1}^{0 σ} \land \dots \land y_{p}^{0 σ} & # x 2264; α$ , i.e. $x_{1}^{ɛ σ} \land \dots \land x_{k}^{ɛ σ} \land y_{1}^{ɛ σ} \land \dots \land y_{p}^{ɛ σ} & # x 2264; α$ , so $x_{1}^{λ δ} \land \dots \land x_{k}^{λ δ} \land y_{1}^{λ δ} \land \dots \land y_{p}^{λ δ} & # x 2264; α$ . If the disjunctive terms g _i1, g _i2, ⋯ , g _{ik
_i} are equal to x _i (or y _h) under the substitution ɛσ in N _i, then g _i1, g _i2, ⋯ , g _{ik
_i} are also equal to x _i (or y _h) under the substitution λ, so all the disjunctive terms that are equal to x _i (or y _h) are g _i1, g _i2, ⋯ , g _{ik
_i}. Therefore, the multi-ary α-semantic resolvent R _i of N and E _j is equal to $R_{i} = N_{1}^{0 λ} \lor N_{2}^{0 λ}$ $\lor \dots \lor N_{k}^{0 λ} \lor E_{j 1}^{0 λ} \lor \dots E_{jp}^{0 λ} \lor α .$ As $v_{D^{0}} (E_{jh}^{0}) & # x 2264; α$ , we have v _{D
⁰} (g ^ɛσ) ≤ α for any disjunctive term g in $E_{jh}^{0}$ , and so v _D (g ^λ) ≤ α. Therefore, we have

$\begin{matrix} R_{i}^{0} & = & N_{1}^{0 σ ɛ} \lor \dots \lor N_{k}^{0 σ ɛ} \lor E_{j 1}^{0 σ ɛ} \lor \dots E_{jp}^{0 σ ɛ} \lor α \\ = & N_{1}^{0 λ ɛ} \lor \dots \lor N_{k}^{0 λ ɛ} \lor E_{j 1}^{0 λ ɛ} \lor \dots E_{jp}^{0 λ ɛ} \lor α \\ = & (N_{1}^{0 λ} \lor \dots \lor N_{k}^{0 λ} \lor E_{j 1}^{0 λ} \lor \dots E_{jp}^{0 λ} \lor α)^{δ} \\ = & R_{i}^{δ} . \end{matrix}$

Hence (N, E ₁, ⋯ , E _q) is a multi-ary α-semantic clash w. r. t. I _D and $G$ and $R_{q}^{0}$ is an instance of R _q, where R _q is a multi-ary α-semantic resolvent of the clash (N, E ₁, ⋯ , E _q).

Theorem 4.4. (Condition Completeness) Let S = C ₁ ∧ C ₂ ∧ ⋯ ∧ C _m, where C ₁, C ₂, ⋯ , C _m are generalized clauses in lattice-valued first-order logic LF (X), I _D = 〈D, μ _D, v _D〉 be an interpretation in LF (X) and α ∈ L, $G$ is an order of generalized literals occurring in these clauses. If the following conditions hold:

S ≤ α;

S ₁ = {C _i|v (C _i) ≤ α} & # x2260 ; ∅ and S ₂ = {C _j|v (C _j)& # x ; α, i ∈ {1, 2, ⋯ , m}} & # x2260 ; ∅;

If g is the leftmost generalized literal of $G$ , then v (g) = α;

Then there exists a multi-ary α-semantic resolution deduction from S to α-empty clause.

Proof. Since S ≤ α, then there exist a ground instance S ^σ of S such that S ^σ ≤ α. As S ₂& # x2260 ; ∅, then there exist i ∈ {1, 2, ⋯ , m} such that v _D (g) & # x2270 ; α for any disjunctive term g in C _i. Therefore, v _{D
⁰} (g ^σ) & # x2270 ; α for any disjunctive term g ^σ of $C_{i}^{σ}$ which is a ground instance of C _i and $C_{i}^{σ} \in S^{σ}$ . From S ₁& # x2260 ; ∅, so there exists C _k ∈ S ₁ such that $v_{D^{0}} (C_{k}^{σ}) & # x 2264; α$ and $C_{k}^{σ} \in S^{σ}$ . It follows from Theorem 3.3 that there exist a multi-ary α-semantic resolution deduction D ⁰ from S ^σ to α-empty clause. From Theorem 4.3, we can lift the D ⁰ to deduction D from S to α-empty clause.

Theorem 4.5. Let S = C ₁ ∧ C ₂ ∧ ⋯ ∧ C _m, where C ₁, C ₂, ⋯ , C _m are generalized clauses in lattice-valued first-order logic L _n F (X), I _D = 〈D, μ _D, v _D〉 be an interpretation in LF (X) and α ∈ L, $G$ is an order of generalized literals occurring in these clauses. If the following conditions hold:

S ≤ α;

There exists an generalized clause C _j such that for any disjunctive term g in C _j, v (g) > α, where j ∈ {1, 2, ⋯ , m};

If g is the leftmost generalized literal of $G$ , then v (g) = α.

Then there exists a multi-ary α-semantic resolution deduction from S to α-empty clause.

Proof. Similar to Theorem 3.4.

Theorem 4.6. Let S be a generalized clause set in lattice-valued first-order logic system LF (X) and α ∈ L. There exist a multi-ary α-semantic resolution deduction w = {Φ ₁, Φ ₂, ⋯ , Φ _t} from S to Φ _t with respect to the interpretation I _D = 〈D, μ _D, ν _D〉 and the order $G$ of generalized literals in LF (X) if and only if there exist a multi-ary α-semantic resolution deduction $w^{0} = {Φ_{1}^{0}, Φ_{2}^{0}, \dots, Φ_{t}^{0}}$ from S ⁰ to $Φ_{t}^{0}$ with respect to the interpretation $I_{D}^{0} = 〈 D^{0}, μ_{D}^{0}, ν_{D}^{0} 〉$ and the order $G^{0}$ of generalized literals in LP (X), where the generalized literals in S ⁰ and $Φ_{i}^{0}$ are the ground instances of the generalized literals in S and Φ _i, respectively.

Proof. The proof of Theorem 4.6 is similar with the The proof of Theorem 3.3, so it is omitted.

Remark 4.1. Theorem 4.6 is called Equivalent Transform Theorem of multi-ary α-semantic resolution in LF (X) and multi-ary α-semantic resolution in LP (X).

Example 4.2. Let C ₁ = P (f (x)) → Q (x) , C ₂ = (P (y ₁) be five generalized clauses in lattice-valued first-order logic L ₆ F (X), where x, y ₁, y ₂, z, μ, v, w ₁, w ₂ are variables and a, b, c are constants. $G : (M (c) \to$ is an order of generalized literals in these generalized clauses. Let S = C ₁ ∧ C ₂ ∧ ⋯ ∧ C ₅ and α = d.

There exist an ground instance substitution

$σ = {a / x, f (a) / y_{1}, c / y_{2}, c / z, b / μ, a / v, b / w_{1}, g (b) / w_{2}}$ such that

$\begin{matrix} C_{1}^{σ} & = & P (f (a)) \to Q (a) \\ C_{σ}^{2} & = & (P (f (a)) \to R (c))^{'} \lor (S (b) \to T (g (b))) \\ C_{σ}^{3} & = & (Q (a)) \to R (c)) \lor (Q (a) \to M (c))^{'} \\ C_{σ}^{4} & = & (S (b) \to T (g (b)))^{'} \\ C_{σ}^{5} & = & (M (c) \to N (a))^{'} \end{matrix}$ i.e. $S^{σ} = C_{1}^{σ} \land C_{2}^{σ} \land \dots \land C_{5}^{σ}$ .

Let I _{D
⁰} = 〈D ⁰, μ _{D
⁰}, v _{D
⁰}〉 be an interpretation of lattice valued first-order logic L ₆ F (X), where D ⁰ = {a, b, c}:

$\begin{matrix} \frac{a}{a}, \frac{b}{b}, \frac{c}{c}, \frac{f (a)}{c}, \frac{g (b)}{c}, \frac{M (c)}{d}, \frac{N (a)}{c}, \\ \frac{P (c)}{b}, \frac{Q (a)}{O}, \frac{S (b)}{b}, \frac{T (c)}{O}, \frac{R (c)}{c} . \end{matrix}$ Under the interpretation I _{D
⁰}, the $v_{D^{0}} (C_{1}^{σ}) & # x 2264; α$ , v _{D
⁰} $(C_{2}^{σ}) & # x 2264; α$ , $v_{D^{0}} (C_{3}^{σ}) & # x 2270; α$ , $v_{D^{0}} (C_{4}^{σ}) & # x 2270; α$ , $v_{D^{0}} (C_{5}^{σ}) & # x 2264; α$ .

Then there exists the following multi-ary α-semantic resolution deduction ω ⁰ from S ^σ to α-empty clause: $\begin{matrix} (1^{0}) C_{1}^{σ} & = & P (f (a)) \to Q (a) \\ (2^{0}) C_{σ}^{2} & = & (P (f (a)) \to R (c))^{'} \lor (S (b) \to T (g (b))) \\ (3^{0}) C_{σ}^{3} & = & (Q (a)) \to R (c)) \lor (Q (a) \to M (c))^{'} \\ (4^{0}) C_{σ}^{4} & = & (S (b) \to T (g (b)))^{'} \\ (5^{0}) C_{σ}^{5} & = & (M (c) \to N (a))^{'} \\ (6^{0}) C_{σ}^{6} & = & (S (b) \to T (g (b))) \lor α by (1^{0}) (2^{0}) (3^{0}) (5^{0}) \\ (7^{0}) C_{σ}^{7} & = & α - empty clause by (4^{0}) (6^{0}) \end{matrix}$ Let I _D = 〈D, μ _D, v _D〉 be an interpretation in lattice value first-order logic L ₆ F (X), where D = {a, b, c}. From the lifting lemma, we have $\begin{matrix} \frac{a}{a}, \frac{b}{b}, \frac{c}{c}, \frac{f (a)}{c}, \frac{f (b)}{c}, \frac{f (c)}{c}, \frac{g (a)}{c}, \frac{g (b)}{c}, \frac{g (c)}{c}, \frac{M (a)}{a_{2}}, \\ \frac{M (b)}{d}, \frac{M (c)}{d}, \frac{S (a)}{b}, \frac{S (b)}{b}, \frac{S (c)}{b}, \frac{T (a)}{O}, \frac{T (a)}{O}, \frac{T (c)}{O}, \\ \frac{R (a)}{c}, \frac{R (b)}{c}, \frac{R (c)}{c} . \end{matrix}$ According to Theorem 4.3, after replacing $C_{i}^{σ} (i = 1, 2, \dots, 5)$ occurring in ω ⁰ with C _i, we have a multi-ary α-semantic resolution deduction ω from S to α-empty clause: $\begin{array}{l} (1) C_{1} = P (f (x)) \to Q (x), \\ (2) C_{2} = (P (y_{1}) \to R (y_{2}))' \lor (S (μ) \to T (g (μ))) \\ \lor (P (f (x)) \to R (c))', \\ (3) C_{3} = (Q (a) \to R (z)) \lor (Q (a) \to M (z))', \\ (4) C_{4} = (S (w_{1}) \to T (w_{2}))' \lor (S (w_{1}) \to T (g (b)))', \\ (5) C_{5} = (M (c) \to N (v))' \\ (6) C_{6} = (S (u) \to T (g (w))) \lor α by (1) (2) (3) (5) \\ (7) C_{7} = α - empty clause by (4) (6) \end{array}$ In fact, there are three multi-ary α-semantic clashes in ω:

$N_{1}^{1} = {C_{3}}, E_{1}^{1} = {C_{1}}, E_{2}^{1} = {C_{2}}, E_{3}^{1} = {C_{5}}$ , the resolvent $R_{2}^{2}$ of clash $(N_{1}^{1}, E_{1}^{1}, E_{2}^{1}, E_{3}^{1},)$ is (S (u) → T (g (w))) ∨ α, where , $N_{2}^{1} = {R_{1}^{1}}$ ;

$N_{1}^{3} = {C_{4}}, E_{1}^{3} = {R_{1}^{3}},$ the resolvent of clash $(N_{1}^{2}, E_{1}^{2})$ is α-empty clause.

Remark 4.2. (1) According to the binary α-resolution principle, the generalized clause (1) occurring in deduction ω does not have a binary α-resolution pair. So there does not exist a binary α-semantic resolution deduction from S to α-empty clause.

(2) From the Example 4.2, the number of generalized literals taking part in multi-ary α-semantic resolution in very multi-ary α-semantic clash is not fixed, this reflects the multi-ary α-semantic resolution deduction is dynamic.

5 Validity analysis of multi-ary α-semantic resolution based on LF (X)

J. F. Zhang introduced the concept of α-semantic clash in LF(X), and the α-semantic resolution deduction and its soundness, the completeness under some conditons are also built. The Definition of α-semantic clash in LF(X) as follows:

Definition 5.1. Let $G$ be an order of generalized literals in generalized clause set S in lattice-valued first-order logic LF (X) and I _D = 〈D, μ _D, ν _D〉 be an interpretation in LF (X). The finite sequence

$(N, E_{1}, E_{2}, \dots, E_{q}) (*)$ is called a α-semantic clash w. r. t. I _D and $G$ , if (*) satisfy the following conditions:

v _D (E _i) ≤ α (i = 1, 2, ⋯ q);

Let R ₁ = N, for any i = 1, 2, ⋯ , q, there exists an α-resolution formula R _α (R _i, E _i);

The α-resolution generalized literals in E _i is the leftmost generalized literals in E _i.

v _D (R _q+1) ≤ α.

R _q+1 is called α-sematic resolvent of this clash w. r. c. I _D and $G$ .

In this section, we will analysis the multi-ary α-semantic resolution method in lattice-value first-order logic LF (X) from the following four aspects:

(1) More effective in expressing complex problem ability. In classical logic, first-order logic has a stronger ability in expressing the problem than propositional logic. Therefore, the lattice-valued first-order with truth in lattice implication algebras have a stronger ability to describe the problem than lattice-valued propositional logic.

(2) More effective in the basis of resolution principle. Many practical problems are often very complex in real world, but there exists certain limitations in processing problem by propositional logic, it is often more natural that using a set of first-order logic formula to describe many practical problems. In order to tackling more complicated problems in real world, Xu. Y etc [21] extend the multi-ary α-resolution principle in lattice-valued propositional logic LP (X) to lattice-valued first-order logic LF (X) with truth in a lattice implication algebra. The multi-ary α-resolution principle based on LF (X) is not only effective promotion of α-resolution principle in lattice-valued logic but also effective extension of multi-ary α-resolution principle in lattice-valued propositional logic LP (X). The multi-ary α-semantic resolution method based on LF (X) is established on basis of multi-ary α-resolution principle based on LF (X). In fact, we have analysis the validity of multi-ary α-resolution principle based on lattice-valued first-order logic LF (X). Therefore, the multi-ary α-semantic resolution method based on LF (X) is more effective than muti-ary α-semantic resolution method based on LP (X).

(3) More effective in reasoning ability. The resolution process and main idea are consistent both α-semantic resolution method and multi α-semantic resolution method based on lattice-valued first-order logic system LF(X) with truth in lattice implication algebra, they are all through control of resolution process to improve the efficiency of reasoning. From Definition 4.1 and Definition 4.3, we can just choose two the generalized literals from α-core andα-electronic, respectively, to take part in the α-resolution in each α-clash of α-semantic resolution in LF(X). But, as far as the multi-ary α-semantic resolution method based on lattice-valued first-order logic LF (X) concerned, some generalized literals (not less than 2) are chosen to take part in multi-ary α-resolution, these generalized literals can divided into two parts, A part of generalized literals from the generalized clause sets which are not less than or not equal to the resolution level α under the interpretation I _D = 〈D,μ_D, ν_D〉, another part of generalized literals from the generalized clause sets which are less than or equal to the resolution level α under the interpretation I_D = 〈D, μ _D, ν_D〉. Therefore, the multi-ary α-semantic resolution method based on LF (X) is more effective in reasoning ability than α-semantic resolution (i.e. 2-ary α-semantic resolution) method based on LF (X), in fact, Example 4.2 also illustrates this point. On the other hand, multi-ary α-semantic resolution method based on lattice valued first-order logic system LF (X) is effectively extension of multi-ary α-semantic resolution method based on the lattice valued propositional logic system LP (X), so multi-ary α-semantic resolution method based on lattice valued first-order logic system LF (X) is more efficient in reasoning ability than multi-ary α-semantic resolution method based on the lattice valued propositional logic system LP (X).

(4) More effective in practicability. In lattice-valued first-order logic LF (X), whether α-semantic resolution deduction or multi-ary α-semantic resolution deduction, they are all complete under some conditions. When J. F. Zhang study the completeness of α-semantic resolution deduction in LF (X), he points out that the completeness of α-semantic resolution deduction need some conditions: (1) Each generalized clause in S should contain propositional variables or negation of propositional variables; (2) If generalized literal g is the most right generalized literal in the generalized literals order $G$ , the v (g) ≤ α, where . These two conditions show that completeness ofα-semantic resolution deduction based on the LF (X) is very limited. But completeness of multi-ary α-semantic resolution deduction based on the LF (X) only need one condition that S can be divided into two non-empty sets under the appropriate interpretation, that is, S is divided into two non-empty sets S ₁ and S ₂ under an interpretation I _D = 〈D, μ _D, v _D〉, where S ₁ is set of generalized clauses which truth are less than or equal to α under an interpretation I _D = 〈D, μ _D, v _D〉, S ₂ is set of generalized clauses which truth are not less than or not equal to α under an interpretation I _D = 〈D, μ _D, v _D〉. It suggests that the completeness of α-semantic resolution deduction in LF (X) need more additional assumptions than the completeness of multi-ary α-semantic resolution deduction. That is to say, in order to achieve the completeness of α-semantic resolution deduction in LF (X) need more other conditions. It also means that the multi-ary α-resolution method is more effective and more flexible thanα-semantic resolution method, completeness of multi-ary α-semantic resolution deductive is more easily obtained than the completeness of α-semantic resolution deduction. Therefore, multi-ary α-resolution method with a wider practicability, stronger reasoning ability and higher reasoning efficiency.

6 Realization for multi-ary α-semantic resolution based on LF (X)

In this section, we will construct the algorithm for multi-ary α-semantic resolution methods based on lattice-valued first-order logic LF (X). Without loss of generality, we assume that S = C ₁ ∧ C ₂ ∧ ⋯ ∧ C _m is a generalized clause set in lattice-valued first-order logical LF (X), where C ₁, C ₂, ⋯ , C _m are generalized clauses of LF (X). In this section, let α ∈ L and α be dual molecules. Now we give an algorithm for multi-ary α-semantic resolution methods based on LF (X). The resolvable generalized literals satisfy the condition (3) in Definition 4.1.

Step 0: Determine an interpretation I _D = 〈D, μ _D, ν _D〉 of generalized clause, an order $G$ of generalized literals in lattice-valued lattice-valued first-order logic LF (X) and set M = {C ∈ S|ν _D (C) ≤ α} , N = {C ∈ S|ν _D (C) & # x2270 ; α}. If M, N& # x2260 ; ∅, turn to Step 1; Otherwise algorithm stops and S cannot be resolved by multi-ary α-semantic resolution methods.

Step 1: Set j = 1;

Step 2: Put A ₀ = ∅ , B ₀ = N;

Step 3: Set i = 0;

Step 4: If A _i contains an α-empty clause, then algorithm stops and S ≤ α; Otherwise, turn to the next step;

Step 5: If B _i =∅, then turn to Step 9; Otherwise, turn to the next step;

Step 6: Put B _i = B ₀ ∪ B ₁ ∪ ⋯ ∪ B _i-1, turn to the next step;

Step 7: Computing the multi-ary α-resolvent of S ₁, S ₂ satisfies the condition (3) in Definition 3.1, where S ₁ ⊆ M, S ₂ ⊆ B ₀ ∪ B ₁ ∪ ⋯ ∪ B _i-1; Denote the set of all multi-ary α-resolvent as W _i+1. If W _i+1 contains an α-empty clause, then algorithm stops; Otherwise, turn to the next step;

Step 8: Let A _i+1 = {Φ ∈ W _i+1|ν _D (Φ) ≤ α}, B _i+1 = {Φ ∈ W _i+1|ν _D (Φ) & # x2270 ; α}; If A _i+1 =∅, then turn to the next step; Otherwise, turn to Step 9;

Step 9: Set i = i + 1, turn to Step 4;

Step 10: Put T = A ₀ ∪ A ₁ ∪ ⋯ ∪ A _i, M = M ∪ T;

Step 11: Set j = j + 1;

Step 12: Computing the multi-ary α-resolvent of S ₁, S ₂ satisfies the condition (3) in Definition 4.1, where S ₁ ⊆ T, S ₂ ⊆ N; Denote the set of all multi-aryα-resolvent as $R$ . If $R$ contains an α-empty clause, then algorithm stops; Otherwise, turn to the nextstep;

Step 13: Let $A_{i + 1} = {Φ \in R | ν_{D} (Φ) & # x 2264; α}; B_{i + 1} = {Φ \in R | ν_{D} (Φ) & # x 2270; α}$ ; Turn to Step 3.

Theorem 6.1. (Soundness) Let S = C ₁ ∧ C ₂ ∧ ⋯ ∧ C _m be a generalized clause set in lattice-valued first-order logic LF (X) and α ∈ L, applying above algorithm on S. If the algorithm terminates in Step 4, then S ≤ α.

Proof. If the algorithm terminates in Step 4, then there exists a multi-ary α-semantic resolution deduction from S to α-empty clause. It follows from Theorem 4.2 that S ≤ α.

Theorem 6.2. (Completeness) Let S = C ₁ ∧ C ₂ ∧ ⋯∧C _m be a generalized clause set in lattice-valued first-order logic LF (X) and α ∈ L, applying above algorithm on S. If S ≤ α, then the algorithm terminates Step 4.

Proof. If S contains α-empty clause, then the α-empty clause must be in M. When i = 0, we can choose some generalized clauses in M and B ₀(i.e. N), respectively, to take part in the multi-ary α-resolution. The multi-ary α-resolvents and α-empty clauses will be in W ₁. It follows from Step 7 that α-empty clauses will be in A ₁, therefore, the algorithm will terminates Step 4.

If S does not contain α-empty clause, the algorithm cannot cycle infinitely. If the algorithm loops infinitely to loop variable i, that is, B _i& # x2260 ; ∅, there is always multi-ary α-resolvent which is not less than or not equal to α under the valuation v in the multi-aryα-resolution deduction. As N is finite, so this case is impossible. If the algorithm loops infinitely to loop variable j, then there is no α-empty clause in the multi-ary α-resolution deduction, which contradicts with S ≤ α. Therefore the algorithm cannot loop infinitely, it must be terminated in Step 4.

Now, we can show the validity of the algorithm by an example:

Example 6.1. Let be five generalized clauses in lattice-valuedfirst-order logic L ₆ F (X), where x, y ₁, y ₂, z, μ, v, w ₁, w ₂ are variables and a, b, c are constants. $G : (M (c) \to N (v))', P (f (x)) \to Q (x), (P (y_{1}) \to R (y_{2}))^{'},$ →R (z)) is an order of generalized literals in these generalized clauses. Let S = C ₁ ∧ C ₂ ∧ ⋯ ∧ C ₅ and α = d.

Let I _D = 〈D, μ _D, v _D〉 be an interpretation in lattice value first-order logic L ₆ F (X), where D = {a, b, c}. From the lifting lemma, we have

$\begin{matrix} \frac{a}{a}, \frac{b}{b}, \frac{c}{c}, \frac{f (a)}{c}, \frac{f (b)}{c}, \frac{f (c)}{c}, \frac{g (a)}{c}, \frac{g (b)}{c}, \frac{g (c)}{c}, \\ \frac{M (a)}{a_{2}}, \frac{M (b)}{d}, \frac{M (c)}{d}, \frac{S (a)}{b}, \frac{S (b)}{b}, \\ \frac{S (c)}{b}, \frac{T (a)}{O}, \frac{T (a)}{O}, \frac{T (c)}{O}, \frac{R (a)}{c}, \frac{R (b)}{c}, \frac{R (c)}{c} . \end{matrix}$ then M = {^{(P(y₁)→R(y₂))^′∨(S(μ)→T(g(μ)))∨(P(f(x))→R(c))^′,(M(c)→N(v))′}} ; N = {P (f (x)) $\begin{matrix} j = 1 : A_{0} & = & \emptyset, B_{0} = N \\ W_{1} & = & {(S (μ) \to T (g (μ))) \lor (Q (a) \to M (c))^{'} \\ \lor α, (Q (a) \to R (c)) \lor α} \\ A_{1} & = & \emptyset \\ B_{1} & = & {(S (μ) \to T (g (μ))) \lor (Q (a) \to M (c))^{'} \\ \lor α, (Q (a) \to R (c)) \lor α} \\ W_{2} & = & {(S (μ) \to T (g (μ))) \lor α} \\ A_{2} & = & {(S (μ) \to T (g (μ))) \lor α} \\ B_{2} & = & \emptyset \\ T & = & {(S (μ) \to T (g (μ))) \lor α} \\ M & = & {C_{2}, C_{5}, (S (μ) \to T (g (μ))) \lor α} \\ j = 2 : R & = & {α} \\ A_{0} & = & {α} \end{matrix}$ From above Example 6.1, we can obtain two multi-ary α-semantic resolvents α, (S (μ) → T (g (μ))) ∨ α by applying multi-ary α-semantic resolution algorithm in LF (X). The result is consistent with Example 4.2 by using multi-ary α-semantic resolution method directly in LF (X).

7 Conclusions

In current paper, we mainly investigated multi-ary α-semantic resolution automated reasoning method based on the multi-ary α-resolution principle for lattice-valued logic with truth-value in a lattice implication algebras. The definitions of the multi-ary α-semantic resolution and multi-ary α-semantic resolution deduction are given, the soundness and completeness are gotten. Meanwhile, the validity of multi-ary α-semantic resolution method is analyzed, the algorithm for multi-ary α-semantic resolution methods based on lattice-valued first-order logic LF (X) is also constructed. In our following work, we will study how to solve some practical problems in real world by α-multi ary semantic resolution automated reasoning. This will become the theoretical foundation for establishing the resolution method and technique with the goal of applying to some practical fields such as expert system design, intelligent robot design, machine learning system design.

Acknowledgments

We would like to thank the anonymous reviewers’ comments and suggestions improved both content and the presentation of this paper. One of reviewer point out many typing mistakes and grammar mistakes in the manuscripts, we gave him (her) heartfelt thanks.

References

10.

11.

12.

13.

14.

15.

16.

17.

18.

19.

20.

21.

22.

23.

24.

25.

26.