Multi-ary α-ordered linear minimal resolution method in lattice-valued logic system 1

Abstract

On the basis of α-minimal resolution principle, an α-n(t)-ary resolution dynamic automated reasoning method—multi-ary α-ordered linear minimal resolution method is studied in lattice-valued propositional logic system LP(X) and lattice-valued first-order logic system LF(X) based on lattice implication algebra (LIA). Firstly, multi-ary α-ordered linear minimal resolution method is established in LP(X), while its theorems of both soundness and completeness are proved. Then, multi-ary α-ordered linear minimal resolution method is further established in the corresponding lattice-valued first-order logic LF(X), along with its soundness theorem, lifting lemma, and completeness theorem. Then, the validity of multi-ary α-ordered linear minimal resolution based on lattice-valued logic is analyzed. At last, an multi-ary α-ordered linear minimal resolution algorithm in LP(X) is designed, and it is proved to be sound and complete, then it is further extended in the corresponding LF(X). This lays the foundation for the further study on α-n(t)-ary resolution dynamic automated reasoning program.

Keywords

Lattice implication algebra lattice-valued logic system resolution dynamic automated reasoning α-minimal resolution

1 Introduction

Since Robinson presented resolution principle based on the classical logic in 1965 [1], automated reasoning based resolution has become an active realm and aroused the interest of many scholars [2 –5]. Many classical resolution methods have also been studied. Particularly, there are three typical resolution methods based on Robinson’s resolution principle, such as semantic resolution, lock resolution and linear resolution [6]. All these methods are devoted to reducing the redundant clauses and improving the resolution efficiency in the course of resolution.

As an important non-classical logic, lattice-valued logic system based on lattice implication algebra provides a strict and reasonable foundation for automated reasoning [7]. Xu et al. (2000 and 2001) introduced α-resolution principle and developed α-resolution deduction in lattice-valued logic based on LIA and proved its soundness and completeness [8, 9]. Compared with resolution principle in Boolean logic, the α-resolution principle in lattice-valued logic based on LIA has new features such as: (a) α-resolution is proceeded at different truth-valued level a (with the possible incomparability) chosen from the truth-valued field—LIA; (b) α-resolution is based on generalized literals, which contain constants and more general implication connective than the one in classical logic. Hence the expressive power is enhanced. Meanwhile, implication connectives in lattice-valued logic are not reducible to other classical logical connectives, which is different from the Kleene implication (i.e., p → q = p′ ∨ q). This irreducibility though semantically justifiable, complicates the calculus; (c) judging whether two generalized literals are α-resolvable should consider both semantic and syntax consistently [8, 9]. As discussed and highlighted in [10], Boolean algebra and Łukasiewicz algebra are special cases of LIA, all the results obtained based on LIA or related logic can be applied into Boolean logic or Łukasiewicz logic accordingly. However, a LIA may not be a Boolean algebra or a Łukasiewicz algebra defined on a chain. LIA is a proper class and includes no-chain algebra as well. Establishing a sound and complete resolution-based reasoning system based on LIA means establishing a sound and complete resolution-based reasoning system based on Boolean algebra and also Łukasiewicz algebra at least. The results obtained in lattice-valued logics based on LIA in several ways have extended and expanded Pavelka fuzzy logic [7, 11]. This shows that the investigation of resolution-based automated reasoning for lattice-valued logic in LIA is worthwhile and is an important extension of classical logic and also some many-valued logics, and is of importance to the research and practitioner community in automated reasoning.

Furthermore, in 2006, Xu et al. [12] established a linguistic truth-valued lattice implication algebra L_V (n ×2) by constructing some linguistic truth values frequently used in daily life. In 2007, Xu et al. [13] established the weak completeness of α-resolution in lattice-valued propositional logic (L_n × L₂) P (X) based on LIA L_n × L₂, and also provided the weak completeness of α-resolution in linguistic truth-valued lattice-valued propositional logic. In 2008, Li et al. [14] studied the properties of α-resolution fields of generalized literals in lattice-valued propositional logic L_n × 2P (X) and the relation between α-resolution in L_n × 2P (X) and that in lattice-valued propositional logic L_nP (X). In order to handle more than two generalized clauses simultaneously, in 2013, Xu et al. [10] extended the α-resolution principle to multi-ary α-resolution principle in lattice-valued logic, which can greatly enhance resolution automated reasoning compared with the ones in classical logic and those proposed in some many-valued logics in terms of soundness and completeness, applicability, reasoning capability and reasoning efficiency. This lays the foundation for the research of resolution dynamic automated reasoning methods.

To further improve the resolution efficiency and reduce redundancy clause, α-n(t)-ary resolution dynamic automated reasoning was proposed in the National Natural Science Foundation of China (Grant No. 61175055) by Xu in 2011. In the processing of α-n(t)-ary resolution, the number of generalized literals n(t) is not taken the fixed number. In order to research α-n(t)-ary resolution dynamic automated reasoning, α-minimal resolution principle which determines how to choose generalized literals in LP(X) and LF(X), as well as its soundness and completeness are introduced in [15]. This is the theoretical guidance for α-n(t)-ary resolution dynamic automated reasoning. Under the guidance of this theory, the corresponding resolution method in LP(X) and LF(X) are researched in this paper. Then, an α-ordered linear minimal resolution algorithm in LP(X) is constructed.

This paper is organized as follows: Section 2 reviews some preliminary relevant concepts about LP(X) and LF(X); In Section 3, multi-ary α-ordered linear minimal resolution method in LP(X) is given, as well as its soundness and completeness; In Section 4, multi-ary α-ordered linear minimal resolution method is further established in the corresponding lattice-valued first-order logic LF(X), along with its soundness theorem, lifting lemma, and completeness theorem; In Section 5, we analysis the validity of multi-ary α-ordered linear minimal resolution method in lattice-valued logic from four aspects; In Section 6, we give a multi-ary α-ordered linear minimal resolution algorithm in LP(X). Thus, it lays the foundation for researching α-n(t)-ary resolution automated program in the future.

This paper is an expansion of paper [21], which has been accepted by The 11th International FLINS Conference on Decision Making and Soft Computing (FLINS 2014).

2 Preliminaries

In this section, we only recall some elementary definitions and properties needed in the following discussions, more detailed notations and results about lattice-valued logic based on LIA and α-resolution principle can be seen in the related References [7 , 20].

2.1 Lattice implication algebra

Definition 2.1. [16] Let (L, ∨ , ∧ , O, I) be a bounded lattice with an order-reversing involution ¢, I and O the greatest and the smallest element of L respectively, and → : L × L → L be a mapping. (L, ∨ , ∧ , ′ , → , O, I) is called a lattice implication algebra if the following conditions hold for any x, y, z ∈ L:

x → (y → z) = y → (x → z),

x → x = I,

x → y = y′ → x′,

x → y = y → x = I implies x = y,

(x → y) → y = (y → x) → x,

(x → y) → z = (x → z) ∧ (y → z) ,

(x → y) → z = (x → z) ∨ (y → z) .

Example 2.1. [7] (Łukasiewicz implication algebra on 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.

Example 2.2. [7] Let L₆ = {O, a, b, c, d, I} , O′ = I, a′ = c, b′ = d, c′ = a, d′ = b, I′ = O, the Hasse diagram of L₆ be defined as Fig. 2.1 and its implication operator be defined as Table 2.1, then (L₆, ∨ , ∧ , → , ′, O, I) is a lattice implication algebra.

Fig.2.1

Hasse Diagram of L₆.

Table 2.1

Implication operator of L₆

→	O	a	b	c	d	I
O	I	I	I	I	I	I
a	c	I	b	c	b	I
b	d	a	I	b	a	I
c	a	a	I	I	a	I
d	b	I	I	b	I	I
I	O	a	b	c	d	I

2.2 Lattice-valued propositional logic LP(X) based on LIA

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

Definition 2.3. [17] The set $F$ of formula of LP(X) is the least set Y satisfying the following conditions:

X ⊆ Y,

L ⊆ Y,

if p, q ∈ Y, then ′ (p) , → (p, q) ∈ Y,

where X is the set of propositional variables, L is the set of constants.

In the following, we denote ‘(p) as p’ and ⟶ (p, q) as p ⟶ q.

Definition 2.4. [17] A mapping v: LP (X) → L is called a valuation of LP(X), if it is a T-homomorphism.

Definition 2.5. [18] Let $G \in F$ and a ∈ L. For any valuation ν of LP(X), if ν (G) ≤ α, we say G is always less than α (or G is α-false), denoted by G ≤ α (or G = a - ⊚).

Definition 2.6. A lattice-valued propositional logical formula G in lattice-valued propositional logic system LP(X) is called an extremely simple form, in short ESF, if a lattice-valued propositional logical formula G^* obtained by deleting any constant or literal or implication term occurring in G is not equivalent to G.

Definition 2.7. [7] A lattice-valued propositional logical formula G in lattice-valued propositional logic system LP(X) is called an indecomposable extremely simple form, in short IESF, if the following two conditions hold:

G is an ESF containing connective → and ^′ at most,

For any $H \in F$ , if $H \in \bar{G}$ in $\bar{LP (X)}$ , then H is an ESF containing connectives → and ^′ at most.

Example 2.3. Suppose that x, y, z, p, q are propositional variables in lattice-valued propositional logic LP(X), b ∈ L. Then, $\begin{matrix} g_{1} & = & (x \to y^{'}) \lor (z \to b) is an ESF; \\ g_{2} & = & x \to y^{'}, g_{3} = z \to b, \\ g_{4} & = & x \to (y \to (p \to q)) are three IESFs . \end{matrix}$

Definition 2.8. [8] All the constants, literals and IESFs in lattice-valued propositional logic system LP(X) are called generalized literals. Here, the definition of literal is the same as that in classical logic.

Definition 2.9. [8] A lattice-valued propositional logical formula G in lattice-valued propositional logic system LP(X) is called a generalized clause if G is a formula of the form $G = g_{1} \lor \dots \lor g_{i} \lor \dots \lor g_{n},$ where g_i are generalized literals, i = 1, 2, …, n

Definition 2.10. [10] (Multi-ary α-Resolution Principle) Let C_i = p_i1 ∨ … ∨ p_{im
_i} be generalized clauses of LP(X), H_i = {p_i1, …, p_{im
_i}} the set of all generalized literals occurring in C_i, i = 1, 2, …, m, a ∈ 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₁ = a) ∨ C₂ (x₂ = a) ∨ … ∨ C_m (x_m = α) is called an m-ary α-resolvent of C₁, C₂, …, C_m, denoted by R_p(m-a) (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.1. [10] (Soundness) Suppose S = C₁ ∧ C₂ ∧ … ∧ C_m, where C₁, C₂, …, C_m are generalized clauses in LP(X), a ∈ L . {Φ₁, Φ₂, …, Φ_t} is a multi-ary α-resolution deduction from S to Φ_t. If Φ_t is a - ⊚, then S ≤ α, i.e., if Φ_t ≤ α, then S ≤ α.

Theorem 2.2. [10] (C ompleteness) Suppose S = C₁ ∧ C₂ ∧ … ∧ C_m, where C₁, C₂, …, C_m are generalized clauses in LP(X). If S ≤ α, then there exist s a multi-ary α-resolution deduction from S to α - ⊚.

2.3 Lattice-valued first-order logic LF(X) based on LIA

Definition 2.11. [9] 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 \subseteq J,$

For any n ∈ N, if f⁽ⁿ⁾ ∈ F, then for any $t_{0}, t_{1}, \dots, t_{n} \in J, f^{(n)} (t_{0}, t_{1}, \dots, t_{n}) \in J .$

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

Definition 2.12. [9] Suppose P is the predicate symbol set in LF(X). The set of atoms of LF(X) is defined as the smallest set 𝒜_t satisfying the following condition:

For any n ∈ N, if P⁽ⁿ⁾ ∈ P, then $P^{(n)} (t_{0}, t_{1}, \dots, t_{n}) \in A_{t}$ for any $t_{0}, t_{1}, \dots, t_{n} \in J$ .

Remark 2.2. P⁽⁰⁾ is specified as a certain element in L.

Definition 2.13. [9] The set of formulas of LF(X) is defined as the smallest set ℱ satisfying the following conditions:

$A_{t} \subset F,$

$If p, q \in F, then p \to q \in F,$

$If p \in F, x is a free variable in p, then (\forall x) p, (\exists x) p \in F .$

Definition 2.14. [9] Suppose $G \in 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 interpretation. An interpretation of G over D is a triple I_D =〈 D, μ_D, ν_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)} \end{matrix}$ is a non-empty set $\begin{matrix} f^{(n)} \mapsto f_{D}^{(n)} (n \in N^{+}), \\ ν_{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 L \\ p^{(n)} \mapsto p_{D}^{(n)} (n \in N^{+}) . \end{matrix}$

Definition 2.15. [7] 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 can not be represented by connectives “∨” or “∧” and G can not be decomposed into a simpler form (G is called an indecomposable implication form).

The disjunction of a finite number of generalized-literals is a generalized-clause. The conjunction of a finite number of generalized-clauses is a generalized-conjunctive normal form.

Definition 2.16. [19] Let C = g₁ ∨ g₂ ∨ … ∨ g_i ∨ … ∨ g_n be a generalized clause. If there exists some equivalent generalized literals in C, then we remain the leftmost generalized literal and delete the other equivalent generalized literals. The above process is called left-combination rule.

Definition 2.17. [19] A generalized clause C is called an ordered generalized clause if the following criterions hold:

C has been simplified by using the left-combination rule;

align by the length of the generalized literals from left to right and put the longest generalized literal on to the leftmost position in C, where the length means the order of the generalized literal (if the order is equivalent, they can be arbitrary arrange);

especially, put the generalized literals containing the constants in front of the constants in C.

Corollary 2.1. [9] Let $G^{*} = G_{1}^{*} \land G_{2}^{*} \land \dots \land G_{m}^{*}$ a generalized-Skölem standard form of a formula G, where $G_{1}^{*}, G_{2}^{*}, \dots, G_{m}^{*}$ are generalized- clauses in LF(X), a ∈ L, and |L| < ℵ ₀. Then G^* ≤ α if and only if there exist $g_{1}^{*}, g_{2}^{*}, \dots, g_{m}^{*}$ such that $g_{1}^{*} \land g_{2}^{*} \land \dots \land g_{m}^{*} \leq a$ , where $g_{i}^{*}$ is an ground instance of $G_{i}^{*}, i = 1, 2, \dots, m$ .

Definition 2.18. [10] (Multi-ary α-Resolution Principle) Let C_i = p_i1 ∨ … ∨ p_{im
_i} be generalized clauses of LF(X), H_i = {p_i1, …, p_{im
_i}} the set of all generalized literals 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}^{σ} \leq α$ , then $C_{1}^{σ} (x_{1}^{σ} = α) \lor C_{2}^{σ} (x_{2}^{σ} = α) \lor \dots \lor C_{m}^{σ} (x_{m}^{σ} = a)$ is called an m-ary α-resolvent of C₁, C₂, …, C_m, denoted by R_f(m-a) (C₁ (x₁) , C₂ (x₂) , …, C_m (x_m)) , x₁, x₂, …, x_m are called an m-ary α-resolution group.

Theorem 2.3. [10] (Soundness) Suppose S = C₁ ∧ C₂ ∧ … ∧ C_m, where C₁, C₂, …, C_m are generalized clauses in L F (X), α ∈ L . {Φ₁, Φ₂, …, Φ_t} is a multi-ary α-resolution deduction from S to Φ_t. If Φ_t ≤ α, then S ≤ α.

Theorem 2.4. [10] (C ompleteness) Suppose S = C₁ ∧ C₂ ∧ … ∧ C_m, where C₁, C₂, …, C_m are generalized clauses in L F (X). If S ≤ α, then there exist s a multi-ary α-resolution deduction from S to α-empty clause.

3 Multi-ary α-ordered linear minimal resolution method in lattice-valued propositional logic system LP(X)

Definition 3.1. Let C_i = p_i1 ∨ … ∨ p_{in_i} be generalized clauses in LP(X), H_i = {p_i1, …, p_{in_i}} the set of all generalized literals occurring in C_i, x_i ∈ H_i, i = 0, 1, 2, …, n . α ∈ L, and C₀ is an ordered generalized clause. If there exists the leftmost generalized literal x₀ in C₀ such that x₀ ∧ x₁ ∧ x₂ ∧ … ∧ x_n ≤ a, but for any j ∈ {1, 2, …, n} , x₀ ∧ x₁ ∧ … ∧ x_j-1 ∧ x_j+1 ∧ … ∧ x_n ≰ α, then C₀ (x₀ = a) ∨ C₁ (x₁ = a) ∨ … ∨ C_n (x_n = a) is called multi-ary α-ordered minimal resolvent of C₀ and {C₁, …, C_n}, denoted by $R_{p (og - a)}^{m} (C_{0} (x_{0}), {C_{1} (x_{1}), \dots, C_{n} (x_{n})})$ , and x₀, x₁, …, x_n are called an multi-ary α-ordered minimal resolution group.

Example 3.1. Let L₉P(X) be lattice-valued propositional logic system based on lattice implication algebra L = (L₉, ∨ , ∧ , ′, → , a₁, a₉), and $\begin{matrix} C_{1} & = & ((q \to a_{8}) \to p)) \lor (p \to q), \\ C_{2} & = & (q \to r) \lor (p \to a_{2}), C_{3} = q \to a_{5}, \\ a \in L_{9} . \end{matrix}$

Take a = a₅ as a resolution level, C₁ is an ordered generalized clause, since there exist the generalized literals such that $((q \to a_{8}) \to p)) \land (p \to a_{2}) \land (q \to a_{5}) \leq a_{5},$ but $((q \to a_{8}) \to p)) \land (p \to a_{2}) ≰ α,$ and $((q \to a_{8}) \to p)) \land (q \to a_{5}) ≰ α$ then a multi-ary α-ordered minimal resolvent of C₁ and {C₂, C₃} is obtained $R_{p (og - a)}^{m} (C_{1}, {C_{2}, C_{3}}) = (p \to q) \lor (q \to r) \lor α .$

Theorem 3.1. In LP(X), let C₀ be an ordered generalized clause, C_i (i = 1, 2, …, n) be generalized clauses, H_i the set of all generalized literals occurring in C_i, α ∈ L. If there exists the leftmost generalized literal x₀ in C₀ and generalized literals x_i ∈ H_i, i = 1, 2, …, n, such that x₀ ∧ x₁ ∧ x₂ ∧ … ∧ x_n ≤ α, and $R_{p (og - a)}^{m} (C_{0} (x_{0}), {C_{1} (x_{1}), \dots, C_{n} (x_{n})})$ is multi-ary α-ordered minimal resolvent of C₀ and {C₁, …, C_n}, then $\begin{matrix} C_{0} \land C_{1} \land C_{2} \land \dots \land C_{n} \\ \leq R_{p (og - a)}^{m} (C_{0} (x_{0}), {C_{1} (x_{1}), \dots, C_{n} (x_{n})}) . \end{matrix}$

Proof. Let C_i = x_i ∨ A_i, B_i = {x_i, A_i} , i = 0, 1, …, n . C₀ is an ordered generalized clause and x₀ is the leftmost generalized literal in C₀, Hence, $\begin{matrix} C_{0} \land C_{1} \land \dots \land C_{n} = (x_{0} \lor A_{0}) \land \dots \land (x_{n} \lor A_{n}) \\ = \underset{(y_{0}, \dots, y_{i}, \dots, y_{n}) \in \prod_{i = 0}^{n} B_{i}}{\lor} (y_{0} \land \dots \land y_{i} \land \dots \land y_{n}) \\ = (x_{0} \land \dots \land x_{i} \land \dots \land x_{n}) \lor \\ \underset{(y_{0}, \dots, y_{i}, \dots, y_{n}) \in \prod_{i = o}^{n} B_{i} - {(x_{0} \land \dots \land x_{i} \land \dots \land x_{n})}}{\lor} \\ (y_{0} \land \dots \land y_{i} \land \dots \land y_{n}) \\ \leq α \lor (A_{0} \lor \dots \lor A_{n}) \\ = (α \lor A_{0}) \lor \dots \lor (a \lor A_{n}) \\ = R_{p (og - a)}^{m} (C_{0} (x_{0}), {C_{1} (x_{1}), \dots, C_{n} (x_{n})}) . \end{matrix}$

Therefore $\begin{matrix} C_{0} \land C_{1} \land \dots \land C_{n} \\ \leq R_{p (og - a)}^{m} (C_{0} (x_{0}), {C_{1} (x_{1}), \dots, C_{n} (x_{n})}) . \end{matrix}$

Definition 3.2. Suppose S be a set of generalized clauses in LP(X), an ordered generalized clause C₀ ∈ S, a ∈ L . {C₀, Φ₁, Φ₂, …, Φ_t} is called a multi-ary α-ordered linear minimal resolution deduction from S to an ordered generalized clause Φ_t (or S can be multi-ary α-ordered linear minimal resolved into Φ_t) (see Fig. 3.1), if

C₀ is a top ordered generalized clause, T_i is a set of side generalized clauses with respect to Φ_i, where i = 0, 1, … , t - 1, Φ₀ = C₀ ;

$Φ_{i} = R_{p (og - a)}^{m} (Φ_{i - 1}, T_{i - 1}), i = 1, \dots, t;$

For any side generalized clause set T_i, T₀ ⊆ S - {C₀} , T_i ⊆ S ∪ {Φ₀, …, Φ_i-1} , i = 1, …, t.

Fig.3.1

Multi-ary α-ordered linear minimal resolution deduction from S to Φ_t.

Theorem 3.2. (Soundness) In LP(X), Suppose S be a set of generalized clauses, an ordered generalized clause C₀ ∈ S, a ∈ L . {C₀, Φ₁, Φ₂, …, Φ_t} is an multi-ary α-ordered linear minimal resolution deduction from S to an ordered generalized clause Φ_t with the top generalized clause C₀. If Φ_t is α - ⊚, then S ≤ α, i.e., if Φ_t ≤ α, then S ≤ α.

Proof. According to Theorem 3.1 and the Definition 3.2, the soundness theorem holds.

Theorem 3.3. (Completeness) Suppose that S = C₀ ∧ C₁ ∧ C₂ ∧ … ∧ C_m, where C₁, C₂, …, C_m are generalized clauses and C₀ is an ordered generalized clause in LP(X), a ∈ L. If S ≤ a and S - {C₀} is α-satisfiable, then there exists a multi-ary α-ordered linear minimal resolution deduction from S to α - ⊚ with the top ordered generalized clause C₀.

Proof. 1. If S only contains one generalized clause C. By S ≤ α, the conclusion holds obviously.

2. If S contains more than one generalized clause. For any i = 1, 2, …, m, Let H_i be the set of all generalized literals occurring in C_i, denote |H_i| = ω_i. Let K(S) be disjunction term number and general clauses in the number of difference, i.e., $K (S) = \sum_{i = 1}^{m} ω_{i} - m$ . Induction of S, the following conditions exist:

If K(S) = 0, then S only consist of unit generalized literals, i.e., every generalized clause contains only one generalized literal in S. Because S ≤ α, so all generalized literals form an α-resolution group. By Theorem 3.1 (Jia 2013), there exists an α-minimal resolution group, we choose anyone of them as an ordered generalized clause, then the conclusion holds.

Assume K(S)<n(n>0) conclusion hold, following we prove K(S) = n conclusion hold.

Let K(S) = n, for top generalized clauses C₀, we have the following 2 situations:

If C₀ is unit generalized clause, set C₀ = g. By K(S) = n, S has one non-unit generalized clause at least, let h be a disjunction term of non-unit generalized clause in S. Set $C_{i} = C_{i}^{*} \lor h$ , and $C_{1}^{*}$ is not empty.

Let $S_{1} = C_{0} \land C_{1} \land \dots \land C_{i - 1} \land C_{i}^{*} \land C_{i + 1} \land \dots \land C_{m}, S_{2} = C_{0} \land C_{1} \land \dots \land C_{i - 1} \land h \land C_{i + 1} \dot{\land} \dots \land C_{m}, S = S_{1} \lor S_{2}$ . Absolutely, S₁ ≤ α, S₂ ≤ α and K (S₁) < n, K (S₂) < n. Then S₁ - {C₀} and S₂ - {C₀} have one is α-satisfiable at least. Let S₁ - {C₀} be α-satisfiable, and K (S₁) < n, then by induction hypothesis, there exists a multi-ary α-ordered linear minimal resolution deduction D₁ from S₁ to α - ⊚ with C₀. Change all $C_{1}^{*}$ in D₁ to C_i, get a deduction $D_{1}^{*}$ . From above know, $D_{1}^{*}$ is a multi-ary α-ordered linear minimal resolution deduction from S, and this deduction get α - ⊚ or α ∨ g.

If $D_{1}^{*}$ is the former, the conclusion holds.

If $D_{1}^{*}$ is the later, due to S₂ ≤ α and K(S₂)<n. By induction assume, there exist a multi-ary α-ordered linear minimal resolution deduction D₂ from S₂ to a - ⊚, and change all h in D₂ to C_i, get deduction $D_{2}^{*}$ . As above, we know $D_{2}^{*}$ deduct to α - ⊚ or $C_{i}^{*} \lor α$ .

If $D_{2}^{*}$ is the former, the conclusion holds.

If $D_{2}^{*}$ is the later, then connect $D_{1}^{*}$ and D₂, and put $D_{1}^{*}$ on the front, then we get a multi-ary α-ordered linear minimal resolution deduction from S to α - ⊚ with C₀.

If C₀ is non-unit generalized clause, set $C_{0} = C_{0}^{*} \lor g_{0}$ , and $C_{0}^{*}$ is not empty. Let $S_{3} = C_{0}^{*} \land C_{1} \land \dots \land C_{m}$ , then S₃ ≤ α and K(S₃)<n. By induction hypothesis, there exists a multi-ary α-ordered linear minimal resolution deduction D₃ from S₃ to α - ⊚ with $C_{0}^{*}$ . Change all $C_{0}^{*}$ in D₃ to C₀, get a deduction $D_{3}^{*}$ . From above know, $D_{3}^{*}$ is a multi-ary α-ordered linear minimal resolution deduction from S with C₀, and this deduction get a - ⊚ or g₀ ∨ α.

If $D_{3}^{*}$ is the former, the conclusion holds.

If $D_{3}^{*}$ is the later, delete the α in last center generalized clause g₀ ∨ α, get deduction D₄. Set S₄ = g₀ ∧ C₁ ∧ … ∧ C_m, then S₄ ≤ α and K(S₄)<n. By induction hypothesis, there exists a multi-ary α-ordered linear minimal resolution deduction D₅ from S₄ to α - ⊚ with g₀. Change all g₀ in D₅ to g₀ ∨ α, get a deduction $D_{5}^{*}$ . Connect $D_{3}^{*}$ and $D_{5}^{*}$ , and put $D_{3}^{*}$ on the front, then we get a multi-ary α-ordered linear minimal resolution deduction from S to α - ⊚ with C₀.

Example 3.2. Let C₁ = x → y, C₂ = (x → z) ′, C₃ = (a₅ → q) ∨ (y → z) ∨ (y → a₂) , C₄ = (p → q) ′ be four generalized clauses in lattice-valued propositional logic L₉P(X), where a₂, a₅ ∈ L₉, x, y, z, p, q are propositional variables, written as S = C₁ ∧ C₂ ∧ C₃ ∧ C₄. If α= a₆, then S ≤ α and there exists a multi-ary α-ordered linear minimal resolution deduction from S to α - ⊚.

According to Definition 3.2, multi-ary α-ordered linear minimal resolution deduction as follows:

Step 1. Set a top generalized clause C₃ and a set C₄ of side generalized clauses such that (a₅ → q) ∧ (p → q) ′ ≤ α, then multi-ary α-ordered linear minimal resolvent $\begin{matrix} D_{1} & = & R_{p (og - a)}^{m} (C_{3}, {C_{4}}) \\ = & (y \to z) \lor (y \to a_{2}) \lor α . \end{matrix}$

Step 2. Set a center generalized clause D₁ and a set {C₁, C₂} of side generalized clauses such that (y → z) ∧ (x → y) ∧ (x → z) ′ ≤ α, then multi-ary α-ordered linear minimal resolvent $D_{2} = R_{p (og - a)}^{m} (D_{1}, {C_{1}, C_{2}}) = (y \to a_{2}) \lor α .$

Step 3. Set a center generalized clause D₂ and a set {C₁, C₂} of side generalized clauses such that (y → a₂) ∧ (x → y) ∧ (x → z) ′ ≤ α, then multi-ary α-ordered linear minimal resolvent $D_{3} = R_{p (og - a)}^{m} (D_{2}, {C_{1}, C_{2}}) = α .$

Example 3.3. Let C₁ = y → b, C₂ = (x → y) ∨ y ∨ (p → q) ′, C₃ = (x → z) ′ ∨ (s → t) , C₄ = (s → t) ′, C₅ = (q → w) ′ be five generalized clauses in lattice-valued propositional logic L₆P(X), where x, y, z, s, t, p, q, w are propositional variables, written as S = C₁ ∧ C₂ ∧ C₂ ∧ C₃ ∧ C₄ ∧ C₅. If α = b, then S ≤ α and there exists a multi-ary α-ordered linear minimal resolution deduction from S to a - ⊚.

Step 1. Set a top generalized clause C₄ and a set C₃ of side generalized clauses such that (s → t) ′ ∧ (s → t) ≤ α, then multi-ary α-ordered linear minimal resolvent $D_{1} = R_{p (og - a)}^{m} (C_{4}, {C_{3}}) = (x \to z)^{'} \lor α .$

Step 2. Set a center generalized clause D₁ and a set {C₁, C₂} of side generalized clauses such that (x → z) ′ ∧ (y → b) ∧ (x → y) ≤ α, then multi-ary α-ordered linear minimal resolvent $D_{2} = R_{p (og - a)}^{m} (D_{1}, {C_{1}, C_{2}}) = (p \to q)^{'} \lor y \lor α .$

Step 3. Set a center generalized clause D₂ and a set C₅ of side generalized clauses such that (p → q) ′ ∧ (q → w) ′ ≤ α, then multi-ary α-ordered linear minimal resolvent $D_{3} = R_{p (og - a)}^{m} (D_{2}, {C_{5}}) = y \lor α .$

Step 4. Set a center generalized clause D₃ and a set C₁ of side generalized clauses such that y ∧ (y → b) ≤ α, then multi-ary α-ordered linear minimal resolvent $D_{4} = R_{p (og - a)}^{m} (D_{3}, {C_{1}}) = α - .$

Its proof figure as follows:

4 Multi-ary α-ordered linear minimal resolution method in lattice-valued first-order logic system LF(X)

Definition 4.1. Let Ci = p_i1 ∨ … ∨ p_{in_i} be generalized clauses in LF(X), H_i = {p_i1, …, p_{in_i}} the set of all generalized literals occurring in C_i, x_i ∈ H_i, i = 0, 1, 2, …, n . a ∈ L, and C₀ is an ordered generalized clause. If there exists the leftmost generalized literal x₀ in C₀ and a substitution σ such that $x_{0}^{σ} \land x_{1}^{σ} \land x_{2}^{σ} \land \dots \land x_{n}^{σ} \leq α$ , but for any $j \in {1, 2, \dots, n}, x_{0}^{σ} \land x_{1}^{σ} \land \dots \land x_{j - 1}^{s} \land x_{j + 1}^{σ} \land \dots \land x_{n}^{σ} ≰ α$ , then $C_{0}^{σ} (x_{0}^{σ} = α) \lor C_{1}^{σ} (x_{1}^{σ} = α) \lor \dots \lor C_{n}^{σ} (x_{n}^{σ} = a)$ is called multi-ary α-ordered minimal resolvent of C₀ and {C₁, … , C_n }, denoted by $R_{f (og - a)}^{m} (C_{0} (x_{0}), {C_{1} (x_{1}), \dots, C_{n} (x_{n})})$ , and x₀, x₁, …, x_n are called a multi-ary α-ordered minimal resolution group.

Example 4.1. Let L₉F(X) be lattice-valued first-order logic system based on lattice implication algebra L = (L₉, ∨ , ∧ , ′, → , a₁, a₉), and $\begin{matrix} C_{1} & = & ((Q (y) \to a_{8}) \to P (x)) \lor (P (x) \to Q (y)), \\ C_{2} & = & (Q (y) \to R (z)) \lor (P (x) \to a_{2}), \\ C_{3} & = & Q (z) \to a_{5}, a \in L_{9} . \end{matrix}$

Take α = a₅ as a resolution level, since there exist the substitution σ = y/z and the generalized literals such that $\begin{matrix} ((Q (y) \to a_{8}) \to P (x)) \land (P (x) \to a_{2}) \\ \land (Q (y) \to a_{5}) \leq a_{5}, \end{matrix}$ but $((Q (y) \to a_{8}) \to P (x)) \land (P (x) \to a_{2}) ≰ a_{5},$ and $((Q (y) \to a_{8}) \to P (x)) \land (Q (y) \to a_{5}) ≰ a_{5} .$ then a multi-ary α-ordered minimal resolvent of C₁ and {C2, C3} is obtained $\begin{matrix} R_{f (og - a)}^{m} (C_{1}, {C_{2}, C_{3}}) \\ = (P (x) \to Q (y)) \lor (Q (y) \to R (y)) \lor α . \end{matrix}$

Theorem 4.1. In LF(X), let C₀ be an ordered generalized clause, C_i (i = 1, 2, …, n) be generalized clauses, H_i the set of all generalized literals occurring in C_i, a ∈ L. If there exists the leftmost generalized literal x₀ in C₀ and generalized literals x_i ∈ H_i (i = 1, 2, …, n) such that under a substitution σ satisfying $x_{0}^{σ} \land x_{1}^{σ} \land x_{2}^{σ} \land \dots \land x_{n}^{σ} \leq α$ , and $R_{f (og - a)}^{m} (C_{0} (x_{0}), {C_{1} (x_{1}), \dots, C_{n} (x_{n})})$ is multi-ary α-ordered minimal resolvent of C₀ and {C₁, …, C_n}, then $\begin{matrix} C_{0} \land C_{1} \land C_{2} \land \dots \land C_{n} \\ \leq R_{f (og - a)}^{m} (C_{0} (x_{0}), {C_{1} (x_{1}), \dots, C_{n} (x_{n})}) . \end{matrix}$ i.e., $\begin{matrix} C_{0} \land C_{1} \land C_{2} \land \dots \land C_{n} \\ \leq C_{0}^{σ} (x_{0}^{σ} = α) \lor C_{1}^{σ} (x_{1}^{σ} = α) \lor \dots \lor C_{n}^{σ} (x_{n}^{σ} = α) . \end{matrix}$

Proof. Similar to Theorem 3.1, we can get the following conclusion: $\begin{matrix} C_{0}^{σ} \land C_{1}^{σ} \land \dots \land C_{n}^{σ} \\ \leq C_{0}^{σ} (x_{0}^{σ} = a) \lor C_{1}^{σ} (x_{1}^{σ} = α) \lor \dots \lor C_{n}^{σ} (x_{n}^{σ} = a) . \end{matrix}$

Since σ is a substitution, so we can obtain $C_{0} \land C_{1} \land \dots \land C_{n} \leq C_{0}^{σ} \land C_{1}^{σ} \land \dots \land C_{n}^{σ} .$

Hence the conclusion holds.

Definition 4.2. Suppose S be a set of generalized clauses in LF(X), an ordered generalized clause C₀ ∈ S, α ∈ L . {C₀, Φ₁, Φ₂, …, Φ_t} is called a multi-ary α-ordered linear minimal resolution deduction from S to an ordered generalized clause Φ_t (or S can be multi-ary α-ordered linear minimal resolved into Φ_t) (see Fig. 3.1), if

C₀ is a top ordered generalized clause, T_i is a set of side generalized clauses with respect to Φ_i, where i = 0, 1, … , t - 1, Φ₀ = C₀ ;

$Φ_{i} = R_{f (og - a)}^{m} (Φ_{i - 1}, T_{i - 1}), i = 1, \dots, t;$

For any side generalized clause set T_i, T₀ ⊆ S - { C₀ } , T_i ⊆ S ∪ {Φ₀, …, Φ_i-1} , i = 1, …, t.

Theorem 4.2. (Soundness) In LF(X), Suppose S be a set of generalized clauses, an ordered generalized clause C₀ ∈ S, a ∈ L . {C₀, Φ₁, Φ₂, …, Φ_t} is a multi-ary α-ordered linear minimal resolution deduction from S to an ordered generalized clause Φ_t with the top generalized clause C₀. If Φ_t is a - ⊚, then S ≤ α, i.e., if Φ_t ≤ α, then S ≤ α.

Theorem 4.3. (Lifting Lemma) Let C₀, C₁, C₂, …, C_n be generalized-clauses without common variables in LF(X), and C₀ is an ordered generalized clause, $C_{i}^{0}$ an instance of C_i, i = 0, 1, 2, …, n. If Ω₀ is a multi-ary α-ordered minimal resolvent of $C_{0}^{0}, {C_{1}^{0}, C_{2}^{0}, \dots, C_{n}^{0}}$ , then there exists a multi-ary α-ordered minimal resolvent Ω of C₀ and {C₁, C₂, …, C_n} such that Ω₀ is an instance of Ω, i.e., Fig. 4.1 holds.

Fig.4.1

Transformation diagram.

Proof. According to the Lifting lemma [15], we can get the conclusion holds easily.

Theorem 4.4. (Completeness) Suppose that S = C₀ ∧ C₁ ∧ C₂ ∧ … ∧ C_n, where C₁, C₂, … C_n are generalized clauses and C₀ is an ordered generalized clause in LF(X), a ∈ L. If S ≤ α and S -{ C₀ } is α-satisfiable, then there exists a multi-ary α-ordered linear minimal resolution deduction from S to α - ⊚ with the top ordered generalized clause C₀.

Proof. In fact, if S ≤ α, then there at least exists a ground instance S^σ of S such that S^σ is α-false by Corollary 2.1. According to Theorem 3.3, there exists a multi-ary α-ordered linear minimal resolution deduction D₀ from S^σ to α - ⊚ with the top ordered generalized clause $C_{0}^{σ}$ . Moreover, we can lift D₀ to a deduction D from S to a - ⊚ with the top ordered generalized clause C₀ by Theorem 4.3.

Example 4.2. C₁ = Q (y) → (P′ (x) → a₅) ′, C₂ = a₇ → R (z) ′, C₃ = (Q′ (y) → a₃) ∨ (b → P (x)) ′, C₄ = P (x) ∨ (R (z) → a₃) , C₅ = (R (a) → Q (y)) ′ be five generalized clauses in lattice-valued first-order logic L₉F(X), where a, b, a_i ∈ L₉ (i = 1, …, 9) , x, y, z are individual variables, P, Q, R are relation symbols, written as S = C₁ ∧ C₂ ∧ C₃ ∧ C₄ ∧ C₅. If α = α₅, then S ≤ α and there exists a multi-ary α-ordered linear minimal resolution deduction from S to α - ⊚.

According to Definition 4.2, multi-ary α-ordered linear minimal resolution deduction as follows:

Step 1. Set a top generalized clause C₅ and a set C₂, C₄ of the side generalized clauses and the substitution σ = {b/y, b/z}, such that

(R (a) → Q (b)) ′ ∧ (a₇ → R (b) ′) ∧ (R (b) → a₃) ≤ α, then the multi-ary α-ordered minimal resolvent $D_{1} = R_{f (og - α)}^{m} (C_{5}, {C_{2}, C_{4}}) = P (x) \lor α .$

Step 2. Set a center generalized clause D₁ and a set {C₁, C₃} of the side generalized clauses and the substitution σ = {b/x, b/y}, such that P (b) ∧ (Q (b) → (P′ (b) → a₅) ′) ∧ (Q′ (b) → a₃) ≤ α, then the multi-ary α-ordered minimal resolvent $D_{2} = R_{f (og - α)}^{m} (D_{1}, {C_{1}, C_{3}}) = (b \to P (b))^{'} \lor α .$

Step 3. Set a center generalized clause D₂ and a set D₁ of the side generalized clauses such that (b → P (b)) ′ ∧ P (b) ≤ α, then the multi-ary α-ordered minimal resolvent $D_{3} = R_{f (og - a)}^{m} (D_{2}, {D_{1}}) = α .$

Example 4.3. Let C₁ = M (f (x)) → N (x) , C₂ = (M (y₁) → R (y₂)) ′ ∨ (S (μ) → T (g (μ))) ∨ (M (f (x)) → R (c)) ′, C₃ = (N (a) → R (z)) ∨ (N (a) → P (z)) ′, C₄ = (S (w₁) → T (w₂)) ′ ∨ (S (w₁) → T (g (b))) ′, C₅ = (P (c) → L (v)) ′ be five generalized clauses in lattice-valued first-order logic L₆F(X), where x, y₁, y₂, z, μ, ν, w₁, w₂ are individual variables, a, b, c ∈ L₆, and M, N, R, S, T, P, L are relation symbols, written as S = C₁ ∧ C₂ ∧ C₃ ∧ C₄ ∧ C₅. If α = d, then S ≤ α and there exists a multi-ary α-ordered linear minimal resolution deduction from S to a - ⊚.

There exist a substitution σ = {a/x, f (a)/y₁, c/y₂, c/z, b/μ, a/v, b/w₁, g (b)/w₂} , and set C₃ as the top generalized clause, we can get the multi-ary α-ordered linear minimal resolution deduction as follows: $\begin{matrix} D_{1} & = & R_{f (og - a)}^{m} (C_{3}, {C_{5}}) = (N (a) \to R (c)) \lor α \\ D_{2} & = & R_{f (og - a)}^{m} (D_{1}, {C_{1}, C_{2}}) \\ = & (S (b) \to T (g (b))) \lor α \\ D_{3} & = & R_{f (og - a)}^{m} (D_{2}, {C_{4}}) = α . \end{matrix}$

Its proof figure as follows:

5 Validity analysis of multi-ary α-ordered linear minimal resolution based on lattice-valued logic

In this section, we will analysis the multi-ary α-ordered linear minimal resolution method in lattice-value logic from the following four aspects:

More effective in expressing complex p roblem ability. The lattice-valued logic with truth in lattice implication algebras have a stronger ability to describe the problem than classical logic.

More effective in the basis of resolution principle. In order to tackling more complicated problems in real world, Xu. Y etc [10] propose the multi-ary α-resolution principle in lattice-valued logic with truth in a lattice implication algebra. The multi-ary α-resolution principle based on lattice-valued logic is effective promotion of α-resolution principle in lattice-valued logic. The multi-ary α-ordered linear minimal resolution method based on lattice-value logic is established on basis of multi-ary α-resolution principle based on lattice-value logic. The validity of multi-ary α-resolution principle based on lattice-valued logic has been analysed. Therefore, the multi-ary α-ordered linear minimal resolution method based on lattice-value logic is more effective than muti-ary α-resolution principle based on lattice-value logic.

More effective in reasoning ability. The resolution process and main idea of multi-ary α-ordered linear minimal resolution method based on lattice-valued logic system with truth in lattice implication algebra is through control the resolution process to improve the efficiency of reasoning. From Definition 3.1 and Definition 4.1, the multi-ary α-ordered linear minimal resolution method based on lattice-value logic choose two or more than two generalized literals to take part in multi-ary α-resolution, not limit to only two generalized literals in each α-resolution. We first select an ordered top generalized literal C₀, and S-C₀ is α-satisfiable, then selecting the generalized literals are no longer blind, it is linear minimal resolution with the direction of the center clause step by step. Every resolution group is the minimal resolution group in each resolution processing. So, comprehensive the above two reasons, multi-ary α-ordered linear minimal resolution method can reduce the generation of redundant clause, and it is more efficient in reasoning ability than 2-ary α-resolution method and some multi-ary α-resolution methods based on lattice-valued logic. In fact, from the above examples, we can see the efficiency of the multi-ary α-ordered linear minimal resolution method.

More effective in practicability. In lattice-valued logic, whether 2-ary α-ordered linear resolution deduction or multi-ary α-ordered linear minimal resolution deduction, they are all complete under some conditions. When W. T. Xu study the completeness of α-ordered linear resolution deduction in lattice-valued logic, he points out that the completeness of α-ordered linear resolution deduction need some conditions: (1) S-C₀ is α-satisfiable; (2) there exist two generalised literals g and h in the different generalised clauses, and g is the leftmost generalised literal in an ordered generalised clause, such that g ∧ h ≤ α, g and h are independent with S* respectively, where S^* = S - {C (g) , C (h)}. But completeness of multi-ary α-ordered linear minimal resolution deduction based on the lattice-valued logic only need one condition that S - {C₀} is α-satisfiable. This suggests that the completeness of α-ordered linear resolution deduction in lattice-valued logic need more additional assumptions than the completeness of multi-ary α-ordered linear minimal resolution deduction. It means that the multi-ary α-ordered linear minimal resolution method is more effective and more flexible than 2-ary α-ordered linear resolution method, the completeness of multi-ary α-ordered linear minimal resolution deduction is more easily obtained than the completeness of 2-ary α-ordered linear resolution deduction. Therefore, multi-ary α-ordered linear minimal resolution method with a wider practicability, stronger reasoning ability and higher reasoning efficiency.

6 An algorithm for multi-ary α-ordered linear minimal resolution method in LP(X)

Based on the multi-ary α-ordered linear minimal resolution method, we can construct an automated reasoning algorithm for this resolution method in lattice-valued propositional logic system.

We suppose that the top generalized clause is unique in S = {C₀, C₁, …, C_i, …, C_m} (if not, we can always select a top generalized clause) in the following algorithm, and denote the set of the side generalized clause with respect to the center generalized clause C by T_C, and denote the number of the side generalized clauses in T_C by |T_C|.

The algorithm is as follows:

Step 0 Set C₀ as the top generalized clause, and S - {C₀} is α-satisfiable.

Step 0.1 For the leftmost generalized literal g₀, search the generalized clauses $B_{i}^{g_{0}}$ such that

$B_{i}^{g_{0}} \in S - {C_{0}};$

If there exist the generalized literal x_i in $B_{i}^{g_{0}}$ such that g₀ ∧ x₁ ∧ … ∧ x_i ∧ … ∧ x_m
₀ ≤ α, and |T_C
₀| is the least (If it is not unique, then select any one of them), where $T_{C_{0}} = {B_{i}^{g_{0}} | i = 1, 2, \dots, m_{0}};$

Otherwise, the algorithm is terminated, the conclusion is S ≰ α.

Step 0.2 Set the side generalized clause set T_{C
₀} and obtain the resolvent $D_{1} = R_{p (og - a)}^{m} (C_{0}, T_{C_{0}})$ .

If D₁ = α - ⊚, then the algorithm is terminated, the conclusion is S ≤ α.

If D₁ ≠ α - ⊚, then add the resolvent D₁ in S such that S₁ = S ∪ {D₁}, go to Step 1.

Step 1. Set D₁ as the center generalized clause.

Step 1.1. For the leftmost generalized literal g₁ in D₁, search the generalized clauses $B_{i}^{g_{1}}$ such that

$B_{i}^{g_{1}} \in S;$

If there exist the generalized literal x_i in $B_{i}^{g_{1}}$ such that g₁ ∧ x₁ ∧ … ∧ x_i ∧ … ∧ x_m
₁ ≤ α, and |T_D
₁| is the least (If it is not unique, then select any one of them), where $T_{D_{1}} = {B_{i}^{g_{1}} | i = 1, 2, \dots, m_{1}};$

Otherwise, the algorithm is terminated, the conclusion is S ≰ α.

Step 1.2. Set T_{D
₁} as the side generalized clause set, and obtain the resolvent $D_{2} = R_{p (og - a)}^{m} (D_{1}, T_{D_{1}})$ .

If D₂ = α - ⊚, then the algorithm is terminated, the conclusion is S ≤ α.

If D₂ ≠ α - ⊚, then add the resolvent D₂ in S₁ such that S₂ = S₁ ∪ {D₂}, go to Step 2.

…

Step k. Set D_k as the center generalized clause.

Step k.1. For the leftmost generalized literal g_k in D_k, search the generalized clauses $B_{i}^{g_{k}}$ such that

$B_{i}^{g_{k}} \in S_{k - 1};$

If there exist the generalized literal x_i in $B_{i}^{g_{k}}$ such that g_k ∧ x₁ ∧ … ∧ x_i ∧ … ∧ x_{m
_k} ≤ α, and |T_{D
_k}| is the least (If it is not unique, then select any one of them), where $T_{D_{k}} = {B_{i}^{g_{k}} | i = 1, 2, \dots, m_{k}}$ ;

Otherwise, the algorithm is terminated, the conclusion is S ≰ α.

Step k.2. Set T_{D
_k} as the side generalized clause set, and obtain the resolvent $D_{k + 1} = R_{p (og - α)}^{m} (D_{k}, T_{D_{k}})$ .

If D_k+1 = a - ⊚, then the algorithm is terminated, the conclusion is S ≤ α.

If D_k+1 ≠ α - ⊚, then add the resolvent D_k+1 in S_k such that S_k+1 = S_k ∪ {D_k+1}, go to Step k + 1.

…

Until the algorithm is terminated.

Theorem 6.1. (Soundness and Completeness of the Algorithm) In LP(X), Suppose S be a set of generalized clauses, S ≤ α if and only if multi-ary α-ordered linear minimal resolution algorithm stops at step k.2.

Proof. (Completness) Set S ≤ α. According to the algorithm, selecting a top generalized clause, take its the leftmost generalized literal g. Based on multi-ary α-ordered linear minimal resolution method, there at least exists a side generalized clause set T = {C₁, …, C_n} belong to S, and generalized literals x_i ∈ C_i (i = 1, …, n), such that g ∧ x₁ ∧ … ∧ x_n ≤ α, that satisfy step 0.1 (2). When determining the side generalized clause set, we can get a multi-ary α-ordered minimal resolvent $R_{p (og - α)}^{m}$ . If the resolvent $R_{p (og - α)}^{m} = α -,$ then algorithm stops at step 0.2. If the resolvent $R_{p (og - α)}^{m} \neq α -$ , then add the resolvent in S, and take the resolvent as center generalized clause, the algorithm go to step 1. According to theorem 3.3, there exists a multi-ary α-ordered linear minimal resolution deduction from S to α - ⊚, then the algorithm stops at step k.2.

(Soundness) Set multi-ary α-ordered linear minimal resolution algorithm stops at step k.2, that is, we get the resolvent $R_{p (og - a)}^{m}$ is α - ⊚ in step k.2, According to theorem 3.2, we get S ≤ α.

Note: If modifying the multi-ary α-ordered linear minimal resolution algorithm in LP(X) slightly, we can get the corresponding algorithm in LF(X).

7 Conclusions

In this paper, an α-resolution method for resolution dynamic automated reasoning based on lattice-valued logic system is studied. Multi-ary α-ordered linear minimal resolution method is presented in lattice-valued logic system based on lattice implication algebra. In a resolution process, a set of side generalized clauses with respect to a center generalized clause is selected, and their multi-ary α-ordered linear minimal resolvent is obtained. Both soundness and completeness theorems are established in LP(X) and LF(X). Then we analysis the validity of multi-ary α-ordered linear minimal resolution method in lattice-valued logic from four aspects. On the basis of the present method of multi-ary α-ordered linear minimal resolution method in LP(X), an automated reasoning algorithm for multi-ary α-ordered linear minimal resolution based on lattice-valued logic system is designed.

Footnotes

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

Robinson

J.A.

, A machine-oriented logic based on the resolution principle [J], Journal of the Association for Computing Machinery 12(1) (1965), 23–41.

Chang

C L.

Lee

R.C.T.

and Symbolic logic and mechanical theorem proving [M]. New York: Academic Press; 1973.

Loveland

D.W.

, Automated theorem proving: A logical basis [M]. Amsterdam, North-Holland; 1978.

Luckham

, Refinements in resolution theory, Proc. IRIA Symp. Automatic Demonstration, Spring-Verlag, New York; 1970, 163–190.

Sofronie

V.S.

Ihlemann

, Automated reasoning in some local extensions of ordered structures [J], Journal of Multiple-Valued Logic and Soft Computing 13(4-6) (2007), 397–414.

Liu

X.H.

, Resolution-based Automated Reasoning [M]. Beijing: Academic Press of China; 1994 (in Chinese).

, Ruan

and Qin

K.Y.

, et al. Lattice-valued logic–an alternative approach to treat fuzziness and incomparability, Berlin: Springer-Verlag; 2003.

, Ruan

and Kerre

E.E.

, et al. α-resolution principle based on lattice-valued propositional logic LP(X) [J], Information Sciences 130 (2000), 195–223.

, Ruan

and Kerre

E.E.

, et al. α-resolution principle based on lattice-valued first-order lattice-valued logic LF(X) [J], Information Sciences 132 (2001), 221–239.

10.

, Liu

and Zhong

X.M.

, et al. Multi-ary α-resolution principle for a lattice-valued logic[J], IEEE Transactions On Fuzzy Systems 21(5) (2013), 898–912.

11.

Pavelka

On fuzzy logic I: Many-valued rules of in-frence, II: Enriched residuated lattices and Semantics of propositional calculi, III: antical completeness of some many-valued propositional calculi [J]. in: Zeitschr. F.Math, Logik und Grundlagend Math 25 (1979), 45–52, 119–134, 447-464.

12.

, Chen

S.W.

and Ma

, Linguistic truth-valued lattice implication algebra and its properties [C] Proc. IMACS Multiconference on “Computational Engineering in Systems Applications” (CESA 2006). Beijing, China; 2006, 1413–1418.

13.

, Chen

S.W.

and Liu

, et al. Weak completeness of resolution in a linguistic truth-valued prepositional logic [C] Proc. IFSA2007: Theoretical Advances and Applications of Fuzzy Logic and Soft Computing, Cancun, Mexico; 2007, 358–366.

14.

X.B.

, Qiu

X.P.

and Chang

Z.Y.

, et al. The properties of α-resolution and J-resolution based on lattice-valued prepositional logic system [J], Chinese Quarterly Journal of Mathematics 6 (2008), 262–269 (in Chinese).

15.

Jia

R.H.

, Xu

and Liu

, α-Minimal resolution principle for a lattice-valued logic [J], Computational Intelligence Systems 8(1) (2015), 34–43.

16.

, Lattice implication algebras [J], Journal of Southwest Jiaotong University 89(1) (1993) 20–27 (in Chinese).

17.

and Qin

K.Y.

, Lattice-valued propositional logic(I) [J], Journal of Southwest Jiaotong University 1(1) (1993) 123–128 (English version).

18.

Qin

K.Y.

, Xu

and Song

Z.M.

, Lattice-valued propositional logic LP(X) (I) [J], Fuzzy Systems and Mathematics 11(4) (1997) 5–10 (in Chinese).

19.

T.W.

and Xu

, α-Ordered linear resolution for lattice-valued logic system based on lattice implication algebra [J], International Journal of Applied Management Science 4(4) (2012), 460–479.

20.

, Zhong

X.M.

, He

X.X.

, et al. Research advances on resolution automated reasoning in lattice-valued logic based on lattice implication algebra [C] The 10th International FLINS Conference on Uncertainty Modeling in Knowledge Engineering and Decision Making (FLINS2012), Istanbul, Turkey, 2012, 714–721.

21.

Jia

H.R.

, He

H.C.

, Xu

, et al. α-Ordered linear minimal resolution method in lattice-valued propositional logic system LP(X) [C] The 11th International FLINS Conference on Decision Making and Soft Computing (FLINS 2014), Paraíba, Brazil; 2014, 191–196.

22.

Liu

, Xu

and Zhong

X.M.

, Multi-ary α-semantic resolution automated reasoning based on lattice-valued first-order logic LF(X) [J], Journal of Intelligent & Fuzzy Systems 29(4) (2015), 1581–1593.