International Journal of Computational Intelligence Systems

<Previous Article In Issue
Download article (PDF)
Next Article In Issue>
Volume 11, Issue 1, 2018, Pages 384 - 401

Non-Clausal Multi-ary α-Generalized Resolution Calculus for a Finite Lattice-Valued Logic

Authors
Yang Xu1, xuyang@home.swjtu.edu.cn, Jun Liu2, j.liu@ulster.ac.uk, Xingxing He1, *, x.he@home.swjtu.edu.cn, Xiaomei Zhong1, zhongxm2013@home.swjtu.edu.cn, Shuwei Chen1, *, swchen@home.swjtu.edu.cn
1School of Mathematics, Southwest Jiaotong University, Chengdu 610031, P.R. China
2School of Computing, Ulster University, Northern Ireland, UK
Corresponding Authors
Received 30 August 2017, Accepted 7 December 2017, Available Online 1 January 2018.
DOI
10.2991/ijcis.11.1.29How to use a DOI?
Keywords
Automated reasoning; Resolution principle; Lattice-valued logic; Lattice implication algebra; Non-clausal multi-ary α-generalized resolution
Abstract

Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α-resolution), a non-clausal multi-ary α-generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.

Copyright
© 2018, the Authors. Published by Atlantis Press.
Open Access
This is an open access article under the CC BY-NC license (http://creativecommons.org/licences/by-nc/4.0/).

1. Introduction

Automatic theorem proving is mechanization of mathematical inference by means of a logic system and inference rules, rather than computation over numbers. The resolution principle is one simple but efficient inference principle, and the resolution calculus is sound and complete in the Boolean logic system. Since its introduction by Robinson in 1965 [1], resolution-based automated reasoning has been extensively studied with the attempt to find natural and efficient proof systems to supporting a wide spectrum of computational tasks [2–5]. A number of important applications of resolution-based automated reasoning systems have been found in many areas such as artificial intelligence [6], logic programming [7, 8], problem solving [9], software model checking and testing [10], data structure verification [11], security protocols automated verification [12], question answering systems [13, 14], inconsistency checking for knowledge based system [15], and so on.

Many-valued logics become increasingly important in computer science and artificial intelligence aiming at establishing the logical foundation of uncertain information processing. Up to now, many researchers have made investigation on resolution-based automated reasoning in the framework of fuzzy logic and many-valued logics, and obtained some important results, refer to Section 4 – Related Work for some details.

To deal with sets of general formulas which can describe complex problems naturally, generalized resolution principle has been put forward for Boolean logic and many-valued logic as well, see [16–21], among others. In generalized resolution, the concept of literal is extended to generalized literal (which is composed by atomic formulas, 0, 1 and logical connectives), the resolvents can be obtained not only by the complementary literals from two conventional clauses, but also atomic formulas from any generalized clauses. It is more natural to retain the original forms in the statement of a theorem rather than transform them into several conjunctive normal forms (CNF). These transformations may produce high amount of new transformed formulas which may increase the complexity of automated reasoning process. In generalized resolution, there is no need to convert the formulas to the corresponding conjunctive normal forms. Meanwhile, the determination of whether two atoms are resolvable can be based on their syntactical form. Therefore, generalized resolution has been recognized as a more efficient proof method in implementation.

The present work focused specially on resolution-based automated reasoning in a many-valued logic L(X) with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA) [22, 23]. In order to handle more than two generalized clauses simultaneously, Xu et al. (2013) [24] extended the α-resolution principle in [25, 26] to multi-ary α-resolution principle in L(X), which can 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. It has specially demonstrated clearly in [24] that binary resolution has limited reasoning capability and also reasoning efficiency especially in many-valued logic.

The above mentioned methods, however, can only deal with the generalized conjunctive normal form (GCNF) in L(X), but cannot handle other general forms of logical formulas. It means that any formula should be transformed into a GCNF in order to conduct the resolution deduction, but such transformation is also a complex process for pretreatment. Inspired from all the above ideas and motivation of generalized resolution in Boolean logic and multi-ary α-resolution in lattice-valued logic, the present paper aims to propose the general generalized α-resolution principle (the reason why it is called “general” and “generalized” will be clarified further in Section 3) in order to deal with complex formulas in finitely lattice-valued logic L(X). This paper is a continuation and extension of the work in [25–33], the binary α-resolution principle introduced in [25, 26] for L(X) is extended to multi-ary α-generalized resolution principle in different ways as follows: (1) the resolution is based on general generalized clauses which is constructed by the generalized literals and logical connectives ″∨, ˄, ′, →, ↔″, instead of the generalized clause containing only ″ ′, →″ in [25, 26]. This, in essential, is a non-clausal resolution; (2) the set of the generalized clauses, which is a complex logical formula, are not necessary to be transformed into the GCNF; (3) the above extended binary α-generalized resolution is further extended into multi-ary α-generalized resolution, i.e., extends the α-generalized resolution pair composed of two generalized literals to the α-generalized resolution group composed of multiple generalized literals based on the work in [24].

The remaining part of this paper is organized as follows. After a brief overview about lattice-valued logic based on LIA in Section 2, the definitions of the general form of α-generalized resolvent and α-generalized resolution deduction in LP(X), along with the discussion of the soundness and completeness of this ground case, are presented in Section 3. In Section 4, the soundness of the general form of α-generalized resolution deduction in LF(X) is given. In order to get the completeness of this general form of α-generalized resolution principle in LF(X), the α-unsatisfiability of the general form of logical formula is discussed. Finally, by Lifting Lemma and the completeness of the ground case, the completeness of the general case is obtained. Section 5 provides a review of some related work. The paper is concluded in Section 6.

2. Preliminaries

In this section, we only recall some elementary definitions, notations and properties needed in the subsequent discussions, more detail s about LIA, lattice-valued logic systems based on LIA and α-resolution principle introduced in those lattice-valued logic systems can be found in [22–26, 28].

2.1 Lattice implication algebra (LIA)

Definition 2.1. [22, 23]

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 (LIA) if the following conditions hold for any x, y, z ∈ L:

  • (I1) x → (y → z) = y → (x → z);

  • (I2) x → x = I;

  • (I3) x → y = y′→ x′;

  • (I4) x → y = y → x = I implies x = y;

  • (I5) (x → y) → y = (y → x) → x;

  • (l1) (x ∨ y) → z = (x → z) ˄ (y → z);

  • (l2) (x ˄ y) → z = (x → z) ∨ (y → z).

Note that Boolean algebra and Łukasiewicz algebra, as two of the most popular logical algebras, are special cases of LIAs. In addition, LIAs form a proper class, and include no-chain algebra and no-Boolean algebra as well. The relationship between LIA with other logical algebraic structure is discussed in [24]. It shows that all the results obtained based on LIA or related logic can be applied into Boolean logic or Łukasiewicz logic at least, as well as other logical algebras. This reflects the fact that the investigation of resolution-based automated reasoning for lattice-valued logic in LIA is worthwhile in terms of generality and applicability.

2.2 Lattice-valued propositional logic LP(X)

Definition 2.2. [23]

Let X be the set of propositional variables, (L, ∨, ˄, ′, →, O, I) be an LIA, T = L ∪ {′,→} be a type with ar(′) = 1, ar(→) = 2 and ar(a) = 0 for any a ∈ L. The proposition logic algebra of the lattice-valued proposition calculus on the set X of propositional variables (in short lattice-valued proposition logic system) is the free T algebra on X and denoted by LP(X).

Remark 2.1.

Note that LP(X) includes the constant formulae (a ∈L), which has been one of the key differences from the most existing many-valued logic systems, because, with the constant formulae included and the implication connective defined differently from the Kleene implication, the syntax in LP(X) is essentially not equivalent to the one in the classical logic any more.

Definition 2.3. [23]

The set Γ of formula of LP(X) is the least set Y satisfying the following conditions:

  1. (1)

    X ⊆ Y;

  2. (2)

    L ⊆Y;

  3. (3)

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

Note that the set of all the L-type fuzzy sets on Γ is denoted by ℱL(Γ). If A∈ ℱL(Γ), for any G∈Γ, A(G)∈L represents the membership degree of G in A.

Definition 2.4. [23]

A mapping γ: (LP(X), ′, →, O) → (L, ′, →, O) is called a valuation of LP(X), if it is a T-homomorphism.

If γ is a valuation of LP(X), we have γ (α) =α for any α∈L. The special element O denotes false in (LP(X), ′, →, O).

Definition 2.5. [25]

Let G ∈ Γ and α ∈ L. For any valuation γ of LP(X), if γ (G) ≤ α, we say G is always less than or equal to α (or G is α-false), denoted by G ≤ α.

2.3 Lattice-valued first-order logic LF(X)

Definition 2.6. [26]

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 𝒥 satisfying the following conditions:

  1. (1)

    V ⊆ 𝒥;

  2. (2)

    For any n ∈ N, if f(n) ∈ F, then for any t1,…, tn ∈ 𝒥, f(n)(t1,…, tn) ∈ 𝒥.

Remark 2.2.

f(0) is specified as a constant symbol.

Definition 2.7. [26]

Suppose P is a 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(n) ∈ P, then P(n)(t0, t1,…, tn) ∈𝒜t for any t0, t1,…, tn ∈ 𝒥.

Remark 2.3.

P(0) is specified as a certain element in L.

Definition 2.8. [26]

The set of formulas of LF(X) is defined as the smallest set ℱ satisfying the following conditions:

  1. (1)

    𝒜t ⊂ ℱ;

  2. (2)

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

  3. (3)

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

Remark 2.4.

Note that p′ = p → O, p ∨ q = (p → q) → q, p ˄ q = (p′ ∨ q′)′, p ↔ q = (p → q) ˄ (q → p). Therefore, if p′, q ∈ ℱ, then p′, p ∨ q, p ˄ q, p ↔ q ∈ ℱ.

Definition 2.9. [26]

Suppose G ∈ ℱ, FG is the set of all functional symbols occurring in G, PG 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 ID = 〈D, µD, νD〉, where,

μD:FG→UD={fD(n):Dn→D|n∈N}
f(0)↦fD(0) , fD(0)(D0)={fD(0)}⊆D , D(0) is a non-empty set
f(n)↦fD(n)(n∈N+),vD:PG→VD={pD(n):Dn→L|n∈N}p(0)↦pD(0),pD(0)(D0)={pD(0)}⊆Lp(n)↦pD(n)(n∈N+).

3. Non-Clausal Multi-ary α-Generalized Resolution Principle for LP(X)

In this section, the outlined work in [29] will be extended and systematized, and further extended into the one for first-order logic LF(X) in Section 4.

In the following, the definition of literal is the same as that in Boolean logic, that is, a literal is either a propositional logic variable l or its negation ~l.

Definition 3.1. [25]

Let G ∈ Γ. G is called an extremely simple form, in short ESF, if G* (∈Γ) obtained by deleting any constant or literal or implication term occurring in G is not equivalent to G.

Definition 3.2. [25]

Let G ∈ Γ. G is called an indecomposable extremely simple form, in short IESF, if the following two conditions hold:

  1. (1)

    G is an ESF containing connectives → and ′ at most;

  2. (2)

    For any H ∈ Γ, if H∈G¯ in LP(X)¯ , then H is an ESF containing connectives → and ′ at most,

LP(X)¯=(LP(X)=,∨,∧,′,→,o¯,I¯) is the LIA, LP(X)=={p¯|p∈LP(X)} , p¯{q|q∈LP(X),q=p} , for any p¯ , q¯∈LP(X)= , p¯∨q¯=p∨q¯ , p¯∧q¯=p∧q¯ , (p¯)′=p′¯ , p¯→q¯=p→q¯ .

Definition 3.3. [25]

All the constants, literals and IESFs in LP(X) are called generalized literals (g-literals). The constants, literals and IESFs in LP(X) are regarded as atomic formulas in LP(X).

Remark 3.1.

In LP(X), a g-literal concept is normally with respect to a specific generalized clause. For example, let C = (x → y) → z) ∨ (z → x), although x → y is a g-literal itself individually, but is not regarded as a g-literal in C, actually (x → y) → z as an IESF is a g-literal in C.

Definition 3.4. [25]

Let G ∈ Γ. G is called a generalized clause (g-clause), if G is a formula of the form below:

G=g1∨…∨gi∨…∨gn
where gi (i = 1, ..., n) are g-literals in G. A conjunction of finite g-clauses is called a generalized conjunctive normal form (GCNF). In this paper, the empty clause is denoted as ∀.

For example, suppose x, y, z, s, t are propositional variables in LP(X), β∈L. Then g1 = x → y, g2 = y → β, g3 = (x → z)′, g4 = s, and g5 = (x → t′) → z are five g-literals; C1 = (x → y) ∨ (y → β), C2 = (x → z)′ ∨ s, C3 = (y → β) ∨ (x → z)′ ∨ ((x → t′) → z) are three g-clauses; and S= C1 ˄ C2 ˄ C3 is a GCNF.

Definition 3.5. [25] (α-Resolution).

Let α∈L, and G1 and G2 be two g-clauses in LP(X) of the forms below respectively:

G1=g1∨…∨gi∨…∨gm,G2=h1∨…∨hj∨…∨hn.
If gi ˄ hj ≤ α, then
G=g1∨…∨gi−1∨gi+1∨…∨gm∨h1∨…∨hj−1∨hj+1∨…∨hn
is called an α-resolvent of G1 and G2, denoted by G = Rα(G1, G2), and gi and hj form an α-resolution pair, denoted by (gi, hj)-α. The generation of an α-resolvent from two clauses, called as α-resolution, is the sole rule of inference of the α-resolution principle, which is a generalization of O-resolution in the classical logic.

Definition 3.6. [25]

In LP(X), suppose a GCNF S = C1 ˄ C2 ˄ … ˄ Cn, α ∈ L. w = {D1, D2, ..., Dm} is an α-resolution deduction from S to a g-clause Dm, if for any i ∈ {1, 2, …, m}

  1. (1)

    Di ∈ {C1, C2, ..., Cn}; or

  2. (2)

    there exist j, k < i, such that Di = Rα(Dj, Dk).

Remark 3.2.

Specially, if there exists an α-resolution deduction from S to a clause which is α-false (also called an α-false clause, denoted by α-□ to differentiate it from that in Boolean logic), then this α-resolution deduction w is called an α-refutation.

Different from some concepts in Boolean logic and also the g-clause in Definition 3.4 in LP(X), in the following, the key concept of this paper is introduced, that is, α-generalized resolution.

A concept of g-clause is recalled in Definition 3.4. It is called “generalized” due to the fact that it is based on the disjunction of g-literals (Definition 3.3), where g-literals could be constants, literals or IESFs in LP(X), and are regarded as atomic formulae. Here we consider more general cases, i.e., general generalized clause, which are actually a composite formula from the g-literals connected by logical connectives ˄, or ∨, or →, or ′ or ↔, that is, they are not limited to atomic formula, could be any single or composite formula, so it is call “general”.

Definition 3.7.

Let g1,..., gn be g-literals in LP(X). A lattice-valued propositional logical formula in LP(X) is called a general generalized ground clause (general g2-clause), denoted by Φ(g1, ..., gn), if it is a composite formula from the g-literals g1 ..., gn connected by logical connectives ˄, or ∨, or →, or ′ or ↔..

We use some examples to clarify the meaning of “general g2-clause”. For example, Φ1 = (y → z)′ ˄ (w → s), Φ2 = (x → y) → z, Φ3=x →((y → a) → t), Φ4 =x∨a, Φ5 =(y → z) ↔ (x → t)′, and Φ6 =((y → z)′ ˄ (w → s)) ∨ ((y → z) ↔ (x → t)′), are all the general g2-clauses, where x, y, z, w, s, t are propositional variables in LP(X), a∈L. Obviously, Φ4 is a g-clause itself. Φ6 is also a general g2-clause although it is a combination of general g2-clauses Φ1 and Φ5, which reflects the meaning of the term “general” here, i.e., any general composite formula by logical connectives ˄, or ∨, or →, or ′ or ↔ can be regarded as a general g2-clause. From this point of view, Φ2 and Φ3 are also g-clauses as in Definition 3.4, but not for Φ1, Φ5 and Φ6.

Based on Definition 3.7, it is easy to say that a composite formula from the g-literals connected by logical connectives ˄, or ∨, or →, or ′ or ↔ can be always transferred into a disjunctive form, and any lattice-valued propositional logical formula in LP(X) can be transferred into a conjunction of finite general g2-clauses. These transformations are based on rules about logical equivalences [23]: the double negative law, the De Morgan’s law and the distributive law between ˄ and ∨.

Here we still use the term “clause” to reflect the similar idea as the one using CNF in Boolean logic. As recalled in Definition 3.4, a conjunction of finite g-clauses is called a generalized conjunctive normal form (GCNF). Accordingly, a conjunction of finite general g2-clauses is called a general generalized ground conjunctive normal form (G3CNF). For example, Φ = ((x → y) → z) ˄ ((y → z)′ ∨ (w → s)) ˄ (x →((y → z) → t)) ˄ ((y → z) ↔ (x → t)′) is a G3CNF, i.e., a conjunction of 4 general g2-clauses, where x, y, z, w, s, t are propositional variables in LP(X).

In essential, although we still use the term “clause” as the part of new concept, which actually is a kind of non-clausal formula compared with the one in Boolean logic.

Definition 3.8.

A general g2-clause G in LP(X) is called a constant g2-clause if all the g-literals in G are all constants. Particularly, if γ(G) = α for any valuation γ of LP(X), then G is called an α-constant g2-clause.

Definition 3.9.

Let Φ be a general g2-clause in LP(X). A g-literal g of Φ is called a local extremely complex form, if

  1. (1)

    g can’t be expanded to a more complex g-literal in Φ by adding → and ′; or

  2. (2)

    If g = g1 ↔ g2, g1 and g2 are g-literals in LP(X), then g is a local extremely complex form as a whole.

Example 3.1.

Let Φ be a general g2-clause in LP(X), Φ = ((x → y) → z) ˄ ((y → z)′ ∨ (w → s)) ˄ (x →((y → z) → t)) ˄ ((y → z) ↔ (x → t)′), where x, y, z, w, s, t are propositional variables in LP(X). For (x → y) → z, the local extremely complex form should not be generalized literals x, y, z, x → y, but (x → y) → z itself. Hence the local extremely complex forms in Φ are (x → y) → z, (y → z)′, w → s, x →((y → z) → t), and (y → z) ↔ (x → t)′.

Remark 3.3.

In the following, all the g-literals discussed are local extremely complex forms.

In the following discussion, we extend α-resolution for LP(X) introduced in [25] to non-clausal multi-ary α-generalized resolution in LP(X), i.e., (1) extend from α-resolution to α-generalized resolution; (2) extend from binary resolution to multi-ary resolution, i.e., the resolved generalized literals extended from two g-literals to the finite g-literals for batch processing clauses, so it can be regarded as a kind of group resolution; and also (3) extend from multi-ary resolution to non-clausal multi-ary resolution. These extensions can improve the efficiency and applicability of α-resolution, and feasible implementation algorithms can be much easier to be established based on it.

Accordingly, the concept of non-clausal multi-ary α-generalized resolution principle is firstly introduced in LP(X), along with the corresponding non-clausal multi-ary α-generalized resolution deduction; its soundness and completeness are also proved afterwards.

Definition 3.10

(Non-clausal n-ary α-generalized resolution). Let Φ1, Φ2,…, Φn be general g2-clauses in LP(X), Hi be the set of g-literals in Φi, α∈L. If there exist general literals gi ∈ Hi (i=1, 2,…, n), such that ∧i=1ngi≤α (i.e., α false), then G=∨i=1nΦi(gi=α) is called a non-clausal n-ary α-generalized resolvent of Φ1, Φ2, …, Φn, denoted by G = Rp(N-n-α)-g (Φ1 (g1), Φ2 (g2), …, Φn (gn)), here “p” means “propositional logic” and “(N-n-α)-g” means “non-clausal n-ary α-generalized” in “Rp(N-n-α)-g”.

Theorem 3.1.

Let Φ1, Φ2,…, Φn be general g2-clauses in LP(X), Hi is the set of g-literals in Φi (i = 1, 2, …, n), α∈L. If there exist g-literals gi ∈ Hi (i = 1, 2, …, n), such that ∧i=1ngi≤α , then

∧i=1nΦi≤Rp(N−n−α)−g(Φ1(g1),Φ2(g2),…,Φn(gn)).

Proof.

It follows from the definition of the general g2-clauses and the logical equivalences in LP(X) that Φi (i = 1, 2, …, n) could be converted to the corresponding generalized conjunction normal forms (GCNF), i.e., Φi=∧j=1niGij , where Gij is a g-clause. Hence, Φi can be rewritten as

Φi=∧j=1niGij=∧j=1mi(gi∨∨g∈Hij−{gi}g)∧G0i,i=1,2,…,n,
where mi is the g-clause number which the g-clause Gij in {Gij|j=1,…, ni} includes gi, Hij is the g-literals set of Gij including gi, and G0i is the conjunction of all Gij (j = 1, 2,..., ni) which doesn’t include gi. Note that
∧i=1n[∧j=1mi(gi∨∨g∈Hij−{gi}g)]=∧i=1ngi∨∨y∈∏i=1n{gi,(∧j=1mi∨g∈Hij−{gi}g)}−{(g1,g2,…,gn)}(∧l=1,zl∈ynzl)        ≤∧i=1ngi∨    ∨i=1n(∧j=1mi∨g∈Hij−{gi}g)≤α∨∨i=1n(∧j=1mi∨g∈Hij−{gi}g),    and
∧i=1nΦi=∧i=1n[∧j=1mi(gi∨∨g∈Hij−{gi}g)∧G0i=∧i=1n[∧j=1mi(gi∨∨g∈Hij−{gi}g)]∧   ∧i=1nG0i,≤[α  ∨  ∨i=1n(∧j=1mi∨g∈Hij−{gi}g]∧∧i=1nG0i=∨i=1n∧j=1mi(α∨∨g∈Hij−{gi}g)∧  ∧i=1nG0i≤∨i=1n[∧j=1mi(α∨∨g∈Hij−{gi}g]∧Gi0]=∨i=1nΦi(gi=α)=Rp(N−n−α)−g(Φ1(g1),Φ2(g2),…,Φn(gn)).

Therefore, ∧i=1nΦi≤Rp(N−n−α)−g(Φ1(g1),…Φn(gn)) .

Remark 3.4.

(1) In the proof of Theorem 3.1, the general g2-clauses should be converted to the corresponding generalized conjunctive normal forms. However, in the course of α-generalized resolution, the general g2-clauses need not to be converted.

(2) If a g-literal which includes many implication connectives is not considered as a local extremely complex form, then Theorem 3.1 may not hold. An example is shown as follows.

Example 3.2. [23]

Let L6 = {O, a, b, c, d, I}, O′ = I, a′ = c, b′ = d, c′ = a, d′ = b, I′ = O, the Hasse diagram of L6 be defined as Figure 3.1 and its implication operator be defined as Table 3.1. Then (L6, ∨, ˄, ′, →, O, I) is an LIA.

Figure 3.1.

Hasse Diagram of L6

→ 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
Table 3.1

Implication Operator of L6

Example 3.3.

Let Φ1 and Φ2 be two general g2-clauses in L6P(X), Φ1 = (b → x)′ → d, Φ2 = (d → x)′ → b, where x is a propositional variable, b, d ∈ L6, and let the resolution level α = a ∈ L6 (see Example 3.2). So Φ1 ˄ Φ2 = ((b → x)′ → d) ˄ ((d → x)′ → b) ≥ (b → d) ˄ (d → b) = a. On the other hand, since (b → x)′ ˄ (d → x)′ ≤ b ˄ d = d < a, if g1 = (b → x)′, g2 = (d → x)′, then Rp(N-2-α)-g (Φ1 (g1), Φ2 (g2)) = (a → d) ∨ (a → b) = b ∨ b = b. However, Φ1 ∧ Φ2 ≰ Rp(N-2-α)-g (Φ1(g1), Φ2(g2)) for a ≰ b.

Definition 3.11.

A lattice-valued propositional logical formula S in LP(X) is called a general g2-clause set or general generalized ground conjunctive normal form (G3CNF) if S is a formula of the form S = Φ1 ˄ Φ2 ˄ … ˄ Φn, where Φi (i = 1, 2, ..., n) are general g2-clauses.

Remark 3.5.

The formula S can also be denoted as S ={Φ1, Φ2, …, Φn} for short.

Definition 3.12.

Suppose S is a G3CNFin LP(X), α ∈ L. Then the sequence D1, D2, … , Dm is called a non-clausal multi-ary α-generalized resolution deduction from S to a general g2-clause Dm, if

  1. (1)

    Di ∈S (i = 1, 2,..., m); or

  2. (2)

    There exist r1, r2,…, rki < i, such that Rp(N-ki-α)-g (Dr1, Dr2, …, Drki) = Di.

If there exists a non-clausal multi-ary α-generalized resolution deduction w from S to the α-false clause (denoted by α-□ similar to the one in Remark 3.2), then w is called a non-clausal multi-ary α-refutation.

Theorem 3.2 (Soundness).

Let S be a set of general g2-clauses in LP(X), α ∈L, the sequence D1, D2, ..., Dm be a non-clausal multi-ary α-generalized resolution deduction from S to a general g2-clause Dm. If Dm = α-□, then S ≤ α.

Proof.

From Definition 3.10 and Theorem 3.1, it is easy to obtain that S = S ˄ D1 ˄ D2 ˄ ... ˄ Dm ≤ Dm = α-□.

Theorem 3.3 (Completeness).

Suppose S is the set of general g2-clauses Φ1, Φ2, …, Φn in LP(X). If S ≤ α, then there exists a non-clausal multi-ary α-generalized resolution deduction from S to α-□.

Proof.

Suppose Hi is the set of g-literals in Φi (i=1, 2, …, n). Let H=∪i=1nHi and |H| be the number of elements in H. We will prove Theorem 3.3 by induction on |H|.

If |H| = 1, then there exists a g-literal g, such that S = g ≤ α. Hence g(g = α) = α, i.e., S can be α -generalized resolved into α-□.

If |H| = 2, then H = {g1, g2}. Hence if S = g1 ˄ g2, we can obtain g1(g1 = α) ∨ g2(g2 = α) = α, i.e., S can be α-generalized resolved into α-∀ If S = g1 ∨ g2, we can obtain the same conclusion.

Suppose that Theorem 3.3 is true for |H| < n (n ≥ 3), we prove it also holds for |H| = n.

Let S = Φ1 ˄ Φ2 ˄ …˄Φn. We consider two cases as follows.

Case 1. If Φi is the conjunction of the g-literals for i =1, 2,…, n, i.e., Φi=∧j=1nigij for i =1, 2,…, n, then S=∧i=1n∧j=1nigij . If S ≤ α, then Rp(N−n−α)−g(Φ1,Φ2,…,Φn)=Rp(N−∏i=1nni−α)−g(g11,g12,…,g1n1,g21,g22,…,g2n2,…,gn1,gn2,…,gnmn)=∧i=1n∧j=1nigij(gij=α)=α . In this case, the conclusion holds.

Case 2. If there exists a general g2-clause Φi0, such that Φi0=Φi0*∨gi0 , where gi0 is a is a g-literal in Φi0, Φi0* includes g-literal. Without loss of generality, suppose i0 = 1, then S=(Φ1*∨g1)∧Φ2∧…∧Φn=(Φ1*∧Φ2∧…∧Φn)∨(g1∧Φ2∧…∧Φn) . Let S1=Φ1*∧Φ2∧…∧Φn , S2 = g1 ∧ Φ2 ∧ … ∧ Φn. Then S1 ≤ α, S2 ≤ α, |HS1| < n, |HS2| < n, where HSk is the set of g-literals in Sk, k =1,2. By induction hypothesis, S1 and S2 respectively have non-clausal multi-ary α-generalized resolution deduction sequences as follows:

  • D11′, D12′, … D′1m1, where D′1m1 is an α-constant g2-clause;

  • D21′, D22′, D′2m2, where D′2m2 is an α -constant g2-clause.

Now we renew Φ1* to Φ1 in D11′, D12′, …, D′1m1, and obtain the α-generalized resolution deduction sequence from S to D1m1 as follows.

D11, D12, …, D1m1, where (1) D1m1 is an α-constant g2-clause; or (2) D1m1 is α ∨ g1.

If D1m1 is α ∨ g1, for the first g-literal g1 in S2, we renew it to α ∨ g1 in D21′, D22′, … D′2m2, and obtain the α-generalized resolution deduction sequence from (α ∨ g1) ˄ Φ2 ˄ …˄ Φn to D2m2 as follows: D21, D22, …, D2m2, where D2m2 is also an α-constant g2-clause.

If it is Case (1), the conclusion holds.

If it is Case (2), then the α-generalized resolution deduction sequence

D11,D12,…,D2m2(=α∨g1),D21,D22,…,D2m2
is the α-generalized resolution deduction from S to α-constant g2-clause.

This completes the proof.

The following two examples provide some illustration of completeness of non-clausal multi-ary α -generalized resolution deduction in LP(X).

Example 3.4.

Let L9 = {ai | 1 ≤ i ≤ 9} be a Łukasiewicz implication algebra (refer to Example 2.3, here n=9), x, y, z, u, v, w propositional variables in L9P(X), S = {x, (x → a2) ∨ (z → v)′ ∨ (u ↔ w), (y → x)′ ∨ (u ↔ w)′, z → a3, a5 → v}. We take the resolution level α = a5, then S ≤ a5. By the completeness of non-clausal multi-ary α-generalized resolution in LP(X) (i.e., Theorem 3.3), there exists a non-clausal multi-ary a5-generalized resolution refutation of S, for example, the one as follows:

  1. (1)

    x

  2. (2)

    (x → a2) ∨ (z → v)′ ∨ (u ↔ w)

  3. (3)

    (y → x)′ ∨ (u ↔ w)′

  4. (4)

    z → a3

  5. (5)

    a5 → v

    -------------------------------

  6. (6)

    a5 ∨ (z → v)′ ∨ (u ↔ w)  by (1), (2)

  7. (7)

    a5 ∨ (u ↔ w)′   by (1), (3)

    -------------------------------

  8. (8)

    a5 ∨ (u ↔ w)   by (4), (5), (6)

    -------------------------------

  9. (9)

    a5-□     by (7), (8)

Moreover, if we judge the α-unsatisfiability of S by α-resolution, we firstly transform S to its generalized conjunctive normal form S1 = {x, (x → a2) ∨ (z → v)′ ∨ (u → w), (x → a2) ∨ (z → v)′ ∨ (w → u), (y → x)′ ∨ (u → w)′ ∨ (w → u)′, z → a3, a5 → v}. We cannot get a binary α-resolution refutation of S1, but can get an alternative multi-ary α-resolution refutation of S1 using the multi-ary α-resolution principle introduced in [24], however which apparently needs more steps or is relatively more complex, i.e.,

  1. (1)

    x

  2. (2)

    (x → a2) ∨ (z → v)′ ∨ (u → w)

  3. (3)

    (x → a2) ∨ (z → v)′ ∨ (w → u)

  4. (4)

    (y → x)′ ∨ (u → w)′ ∨ (w → u)′

  5. (5)

    z → a3

  6. (6)

    a5 → v

    -------------------------------

  7. (7)

    a5 ∨ (z → v)′ ∨ (u → w)  by (1), (2)

  8. (8)

    a5 ∨ (z → v)′ ∨ (w → u)  by (1), (3)

  9. (9)

    a5 ∨ (u → w)′ ∨ (w → u)′  by (1), (4)

    -------------------------------

  10. (10)

    a5 ∨ (u → w)   by (5), (6), (7)

  11. (11)

    a5 ∨ (w → u)    by (5), (6), (8)

    -------------------------------

  12. (12)

    a5 ∨ (w → u)′   by (9), (10)

  13. (13)

    a5-□     by (11), (12)

Example 3.5.

Let (L6, ∨, ˄, ′, →, O, I) be an LIA as defined in Example 3.2, x, z, s, t propositional variables in L6P(X), S = {x, (x → a), (x → b) ∨ (t → d), (s ↔ t) ∨ (z → t), (s ↔ t)′, (z → c)′}. We take the resolution level α = d, then S ≤ d. By the completeness of non-clausal multi-ary α-generalized resolution in LP(X), there exists a non-clausal multi-ary d-generalized resolution refutation of S, for example, the one as follows:

  1. (1)

    x

  2. (2)

    x → a

  3. (3)

    (x → b) ∨ (t → d)

  4. (4)

    (s ↔ t) ∨ (z → t)

  5. (5)

    (s ↔ t)′

  6. (6)

    (z → c)′

    -------------------------------

  7. (7)

    d ∨ (t → d)   by (1), (2), (3)

  8. (8)

    d ∨ (z → t)    by (4), (5)

    -------------------------------

  9. (9)

    d-□    by (6), (7), (8)

Similarly, if we judge the α-unsatisfiability of S by α-resolution principle, we firstly transform S to its generalized conjunctive normal form S1 = {x, (x → a), (x → b) ∨ (t → d), (s → t) ∨ (z → t), (t → s) ∨ (z → t), (s → t)′ ∨ (t → s)′, (z → c)′}. We cannot get a binary α -resolution refutation of S1, but can get a relatively complex multi-ary α-resolution refutation of S1 [Xu et al. 2013], i.e.,

  1. (1)

    x

  2. (2)

    (x → a)

  3. (3)

    (x → b) ∨ (t → d)

  4. (4)

    (s → t) ∨ (z → t)

  5. (5)

    (t → s) ∨ (z → t)

  6. (6)

    (s → t)′ ∨ (t → s)′

  7. (7)

    (z → c)′

    -------------------------------

  8. (8)

    d ∨ (t → d)   by (1), (2), (3)

    -------------------------------

  9. (9)

    d ∨ (s → t)   by (4), (7), (8)

  10. (10)

    d ∨ (t → s)′   by (5), (7), (8)

    -------------------------------

  11. (11)

    d ∨ (t → s)′    by (6), (9)

    --------------------------------

  12. (12)

    d-□    by (10), (11)

From the above two examples show that there is no need to transform those complex formula into the generalized conjunctive normal form (actually it is not straightforward for the transformation), so that means “non-clausal” resolution. Theorem 3.2 and Theorem 3.3 show that the non-clausal multi-ary α-generalized resolution deduction in LP(X) is sound and complete, along with Examples 3.4 and 3.5 to illustrate the distinct advantages of non-clausal multi-ary α-generalized resolution in terms of reasoning capability and efficiency. Furthermore, for an α-unsatisfiable set of general g2-clauses in LP(X), if we convert it into the corresponding generalized conjunctive normal form, and judge it by the α-resolution principle, then it may not lead to a binary α-resolution refutation partially because its restriction of the number of α-resloved literals is 2. Although sometimes it may lead to a multi-ary α-resolution refutation using the method in [24], it is more complex than the non-clausal multi-ary α-resolution refutation introduced in this paper.

4. Non-Clausal Multi-ary α-Generalized Resolution Principle for LF(X)

In this section, non-clausal multi-ary α-generalized resolution principle is extended from LP(X) to LF(X), as extended and systematized version of [30]. The α-unsatisfiability for a general form of the logical formula, i.e., general g-clause in LF(X) is discussed firstly. Then, Lifting Lemma of the non-clausal multi-ary α-generalized resolution principle for LF(X) is established, and the soundness of this general case is shown. Finally, by the completeness of the ground case, we lift it to the general case in LF(X), i.e., the completeness for this general form of non-clausal multi-ary α-generalized resolution deduction for LF(X).

4.1 α- unsatisfiability for a general form of the logical formula in LF(X)

Definition 4.1. [26]

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

  1. (1)

    G is a literal; or

  2. (2)

    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).

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 4.2. [26]

Let G ∈ℱ, α ∈ L. G is said to be α-false, if νD(G) ≤ α for any interpretation ID = 〈D, µD, νD〉 of G.

Definition 4.3. [26]

Suppose G is a formula of the form Q1x1…QnxnG*, where Q1,…, Qn 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 4.4. [26]

Suppose a formula G = Q1x1…QnxnM is a generalized-prenex conjunctive normal form. The formula G* obtained by the following steps is called a generalized-Skolem normal form of G:

  1. (1)

    If Qr is an existential quantifier and without any universal quantifier occurring ahead it in the prefix Q1,…, Qn (from left to right), we choose a new constant c different from other constants occurring in M, replace all xr occurring in M by c, and then delete Qr from the prefix Q1,…, Qn.

  2. (2)

    If Qr is an existential quantifier and Qk1,…,Qkm are all the universal quantifiers occurring ahead Qr (m ≥ 1, 1 ≤ k1 < …< km < r), we choose a new m-ary function symbol fmG different from all other function symbols occurring in M, replace all xr in M by fmG(xk1,…,xkm) and then delete Qr from the prefix Q1,…, Qn.

  3. (3)

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

Definition 4.5.

Let g1, g2, ..., gn be g-literals in LF(X). A logical formula F in LF(X) is called a general g-clause if these g-literals are connected by logical connectives ˄, ∨, →, ′ and ↔, denoted by Φ(g1, g2,..., gn).

Definition 4.6.

A general g-clause in LF(X) is called a constant g-clause if it contains only constants. Particularly, for a constant g-clause G, if νD (G) = α for any interpretation ID = <D, µD, νD>, it follows that then this constant g-clause G is called an α-constant g-clause.

The conjunction of finite general g-clauses is a general g-conjunctive normal form. Similar to α -resolution principle in LF(X) [26], we can formally give definitions of general g-prenex normal form, general g-prenex conjunction normal form, general g-Skolem normal form, etc. Also, the definitions such as substitution, the most general unifier, ground substitution, instance, ground instance occurring in the following are the same as those in Boolean logic.

Definition 4.7.

Let Φ be a general g-clause in LF(X). A g-literal g of Φ is called a local extremely complex form, if

  1. (1)

    g can’t be expanded to a more complex g-literal in Φ by adding → and ′; or

  2. (2)

    If g = g1 ↔ g2, g1 and g2 are g-literals in LF(X), then g is a local extremely complex form as a whole.

Remark 4.1.

In the following, all the g-literals discussed are local extremely complex forms.

Here, the g-clause is extended to the general g-clause, i.e., the general g-clause may not be the disjunction of the g-literals; it seems that it’s too complex to explore the α-unsatisfiability of the logical formula in LF(X). Fortunately, note that every variable in the general g-Skolem normal form is universally quantified, and many properties of formulas in LF(X) do not rely on the structure of the g-clauses, many conclusions in the g-Skolem normal form still hold for general form as far as α-unsatisfiability is concerned. We only state main results as follows.

Theorem 4.1.

Let G and G* be two logical formulas in LF(X), and G* a general g-Skolem normal form of G, α ∈ L. Then G is α-false if and only if G* is α-false.

Proof.

It is obvious from Theorem 2.1 in [26].

Theorem 4.2.

Suppose G* is a general g-Skolem normal form of a formula G in LF(X). If an interpretation ID = <D, µD, νD> α-satisfies G*, then the H-interpretation IH = <H, µH, νH> of G* corresponding to ID also α-satisfies G*.

Proof.

It is obvious from Theorem 3.1 in [26].

Theorem 4.3.

Suppose G* is a general g-Skolem normal form of a formula G in LF(X). Then G* is α-false if and only if νH(G*) ≱ α holds for all H-interpretations IH = <H, µH, νH > of G*.

Proof.

It is obvious from Theorem 3.2 in [26].

Theorem 4.4.

Suppose G* is a general g-Skolem normal form of a formula G in LF(X), |L|<+ ∝. Then G* is α-false if and only if there exists K∈Ν such that νH(G*)≱ α holds for every adjoint νH of every element in LK.

Proof.

It is obvious from Theorem 3.3 in [26].

Theorem 4.5.

Suppose G* is a general g-Skolem normal form of a formula G in LF(X), |L|<+∝. Then G* is α-false if and only if there exists a finite ground instance set G*0 of G* such that Gc*0 is α-false, where Gc*0 is the conjunction of all ground instances of G*0.

Proof.

It is obvious from Theorem 3.4 in [26].

From Theorem 4.5, in order to judge the α-unsatisfiability of a formula in LF(X), when |L|<+∝, we only need to find a finite and ground instance set of this formula, and validate its α-unsatisfiability. Hence it is relatively achievable.

4.2 Soundness and completeness for the general form of non-clausal multi-ary α-generalized resolution deduction in LF(X)

This section provides the soundness and completeness for the general form of the non-clausal multi-ary α-generalized resolution deduction in LF(X).

Definition 4.8.

Let Φ be a general g-clause in LF(X). If there exists a most general unifier σ of g-literals g1, g2, ..., gm in Φ, then Φσ is called a factor of Φ.

Definition 4.9

(A general form of non-clausal multi- ary α-generalized resolution). Let Φ1, Φ2, …, Φn be general g-clauses in LF(X), Φ1σ1 be a factor of Φ1 for g-literals g11, g12, … g1r1, Φ2σ2 be a factor of Φ2 for g-literals g21, g22, …, g2r2, … and Φ2σn be a factor of Φn for g-literals gn1, gn2, … gnrn, α∈ L. If ∧i=1ngi1σi≤α (i.e., α false), then G=∨i=1nΦiσi(gi1σi=α) is called a non-clausal n-ary α-generalized resolvent of Φ1, Φ2, …, Φn, denoted by G = Rf(N-n-α)-g (Φ1, Φ2, …, Φn), here “f” means “first-order logic”.

Definition 4.10.

Suppose S is a general g-clause set in LF(X), α ∈ L, the sequence D1, D2, ..., Dm is called a non-clausal multi-ary α-generalized resolution deduction from S to general g-clause Dm, if

  1. (1)

    Di ∈ S (i = 1, 2, ..., m); or

  2. (2)

    There exist r1, r2,.…, rki < i, such that Rf(N-ki-α)-g (Dr1, Dr2, … Drki = Di.

The usual method for proving the completeness of a version of resolution has two steps. Firstly, one proves the ground case in propositional logic, in which no variables occur. Then one lifts it to the general case in first-order logic.

In the Proof of Theorem 5.3 (Lifting Lemma) for generalized clause in LF(X) [24], the disjunction of g-literals was not used, so Theorem 4.6 also holds.

Theorem 4.6

(Lifting Lemma). If Φ01,Φ02,...,Φ0n are instances of general g-clauses Φ1, Φ2,…, Φn in LF(X), respectively, P0 is a non-clausal multi-ary α-generalized resolvent of Φ01,Φ02,...,Φ0n, then there exists a non-clausal multi-ary α-generalized resolvent P of Φ1, Φ2,…, Φn such that P0 is an instance of P.

Theorem 4.7.

Let Φ1, Φ2,…, Φn be general g-clauses in LF(X), Φ1σ1 be a factor of Φ1 for g-literals g11, g12, …, g1r1, Φ2σ2 be a factor of Φ2 for g-literals g21, g22, … g2r2, …, and Φnσn be a factor of Φn for g-literals gn1, gn2, …, gnrn, α ∈L. If ∧i=1ngi1σi≤α (i.e., α false), then

∧i=1nΦi≤∨i=1nΦiσ1(gi1σi=α).

Proof.

Similar to the proof of Theorem 3.1, for most general unifiers σi (i = 1, 2, …, n), if ∧i=1ngi1σi≤α , then ∧i=1nΦiσi≤∨i=1nΦiσi(gσii1=α) . Hence, it follows from ∧i=1nΦi≤∧i=1nΦiσi that ∧i=1nΦi≤∨i=1nΦiσi(gi1σi=α) .

Theorem 4.8 (Soundness).

Let S be a general g-clause set in LF(X), α ∈L. The sequence Φ1, Φ2, ..., Φm be a non-clausal multi-ary α-generalized resolution deduction from S to general g-clause Φm. If Φm = α-∀, then S ≤ α, i.e., S is α false.

Proof.

According to Theorem 4.7, similar to the proof of Theorem 3.2, we can easily get the conclusion.

Theorem 4.9 (Completeness).

Suppose S is the set of general g-clauses Φ1, Φ2, …, Φn in LF(X), |L|<+∝. If S ≤ α (i.e., S is α false), then there exists a non-clausal multi-ary α-generalized resolution deduction from S to α-□.

Proof.

By Theorem 4.5 and S ≤ α, there exists a finite ground instances set S0 of S such that S0 ≤ α. By Theorem 3.3, there exists a ground non-clausal multi-ary α-generalized resolution deduction from S0 to α-□. By Lifting Lemma (Theorem 4.6), there exists a non-clausal multi-ary α-generalized resolution deduction from S to α-□.

The following two examples provide some illustration of completeness of non-clausal multi-ary α-generalized resolution deduction in LF(X).

Example 4.1.

Let Λ9 = (L9, ∨, ˄, ′, →, a1, a9) be a Łukasiewicz implication algebra, b, c, d constants, x, y, w, r, s, t variables in L9F(X), S = {(P(s) ↔ Z1(y)), (P(s) ↔ Z1(y))′ ∨ (T(t) → W(w)), ((T(t) → W(w))→ a2) ∨ (Z2(s) → R(r)), (Q(y) → Z1(b)) ∨ (R(r) → Z1(c))′, R(r) → Z1(d), (a3 → Q(y))′}. If we take the resolution level α = a6, then S ≤ α. By the completeness of non-clausal multi-ary a6-generalized resolution (Theorem 4.9), there exists a non-clausal multi-ary a6-generalized resolution refutation from S.

In fact, we take a ground substitution σ ={a / x, b / t, c / w, a / s, c / y, b / r} of S, then Sσ = {(P(a) ↔ Z1(c)), (P(a) ↔ Z1(c))′ ∨ (T(b) → W(c)), ((T(b) → W(c))→ a2) ∨ (Z2(a) → R(b)), (Q(c) → Z1(b)) ∨ (R(b) → Z1(c))′, R(b) → Z1(d), (a3 → Q(c))′}, and Sσ ≤ a6, then there exists a non-clausal multi-ary α-generalized resolution refutation ω0 from Sσ in L9P(X) as follows:

  1. (1)

    P(a) ↔ Z1(c)

  2. (2)

    (P(a) ↔ Z1(c))′ ∨ (T(b) → W(c))

  3. (3)

    ((T(b) → W(c))→ a2) ∨ (Z2(a) → R(b))

  4. (4)

    (Q(c) → Z1(b)) ∨ (R(b) → Z1(c))′

  5. (5)

    R(b) → Z1(d)

  6. (6)

    (a3 → Q(c))′

    -------------------------------

  7. (7)

    a6∨(P(a)↔ Z1(c))′ ∨ (Z2(a)→R(b)) by (2), (3)

  8. (8)

    a6 ∨ (R(b) → Z1(c))′   by (4), (6)

    -------------------------------

  9. (9)

    a6 ∨ (Z2(a) → R(b))   by (1), (7)

    -------------------------------

  10. (10)

    a6-□ by (5), (8), (9)

By Lifting Lemma of non-clausal multi-ary α -generalized resolution, there exists a non-clausal multi-ary α -generalized resolution refutation ω from S in L9F(X), that is, we resume the variable symbols in S which are substituted by σ in Sσ. Therefore, the non-clausal multi-ary α-generalized resolution refutation of S is:

  • (P(s) ↔ Z1(y)),

  • (P(s) ↔ Z1(y))′ ∨ (T(b) → W(c)),

  • ((T(b) → W(c))→ a2) ∨ (Z2(a) → R(b)),

  • (Q(c) → Z1(b)) ∨ (R(b) → Z1(c))′,

  • R(b) → Z1(d),

  • (a3 → Q(y))′,

  • a6 ∨ (P(x) → (P(x) → Z1(c))) ∨ (Z2(s) → R(r)),

  • a6 ∨ (R(r) → Z1(d))′,

  • a6 ∨ (Z2(s) → R(r)),

  • a6-□.

Furthermore, if we judge the α-unsatisfiability of S by α-resolution principle, we firstly transform S to its generalized conjunctive normal form S1 = {P(s) → Z1(y), Z1(y) → P(s), (P(s) → Z1(y))′ ∨ (Z1(y) → P(s))′ ∨ (T(t) → W(w)), ((T(t) → W(w))→ a2) ∨ (Z2(s) → R(r)), (Q(y) → Z1(b)) ∨ (R(r) → Z1(c))′, R(r) → Z1(d), (a3 → Q(y))′}.

Then we take a ground substitution σ ={a / x, b / t, c / w, a / s, c / y, b / r} of S1, then S1σ = {P(a) → Z1(c), Z1(c) → P(a), (P(a) → Z1(c))′ ∨ (Z1(c) → P(a))′ ∨ (T(b) → W(c)), ((T(b) → W(c))→ a2) ∨ (Z2(a) → R(b)), (Q(c) → Z1(b)) ∨ (R(b) → Z1(c))′, R(b) → Z1(d), (a3 → Q(c))′}, and S1σ ≤ a6. We cannot get a binary α -resolution refutation of S1σ, but can get a relatively complex multi-ary α -resolution refutation [24] of S1σ, i.e., there exists a multi-ary α -resolution refutation ω0 from S1σ in L9P(X) as follows:

  1. (1)

    P(a) → Z1(c)

  2. (2)

    Z1(c) → P(a)

  3. (3)

    (P(a)→Z1(c))′∨ (Z1(c)→P(a))′∨ (T(b)→ W(c))

  4. (4)

    ((T(b) → W(c))→ a2) ∨ (Z2(a) → R(b))

  5. (5)

    (Q(c) → Z1(b)) ∨ (R(b) → Z1(c))′

  6. (6)

    R(b) → Z1(d)

  7. (7)

    (a3 → Q(c))′

    -------------------------------

  8. (8)

    a6 ∨ (Z1(c)→P(a))′ ∨ (T(b)→W(c))  by (1), (3)

    -------------------------------

  9. (9)

    a6 ∨ (T(b) → W(c))    by (2), (8)

    -------------------------------

  10. (10)

    a6 ∨ (Z2(a) → R(b))    by (4), (9)

    -------------------------------

  11. (11)

    a6 ∨ (R(b) → Z1(c))′    by (5), (10)

    -------------------------------

  12. (12)

    a6-□     by (6), (7), (11)

Similarly, by Lifting Lemma of multi-ary α -resolution, there exists a multi-ary α -resolution refutation ω from S1 in L9F(X), that is, we resume the variable symbols in S1 which are substituted by σ in S1σ. Therefore, the multi-ary α-resolution refutation ω of S1 is:

  • P(s) → Z1(y),

  • Z1(y) → P(s),

  • (P(s) → Z1(y))′ ∨ (Z1(y) → P(s))′ ∨ (T(t) → W(w)),

  • ((T(t) → W(w))→ a2) ∨ (Z2(s) → R(r)),

  • (Q(y) → Z1(b)) ∨ (R(r) → Z1(c))′,

  • R(r) → Z1(d),

  • (a3 → Q(y))′,

  • a6 ∨ (Z1(y) → P(s))′ ∨ (T(t) → W(w)),

  • a6 ∨ (T(t) → W(w)),

  • a6 ∨ (Z2(s) → R(r)),

  • a6 ∨ (R(r) → Z1(c))′,

  • a6-□.

Example 4.2.

Let (L6, ∨, ˄, ′, →, O, I) be an LIA defined as Example 2.4, a, c, d ∈ L6, x, y, z, t, w, u variable symbols in L6F(X), S = {P(x), (P(x)→ d) ∨(Z1(w) ↔ Q(y)), (Z1(w) ↔ Q(y))′ ∨ (T(z) → d), Z(t) → T(z), (Z(t) → Z1(u))′}. If we take the resolution level α = d, then S ≤ d. By the completeness of non-clausal multi-ray d-generalized resolution (Theorem 4.9), there exists a non-clausal multi-ray d-generalized resolution refutation from S.

In fact, we take a ground substitution σ ={a1 / x, a2 / y, a3 / z, a4 / t, a5 / u, a1 / w} of S, where a1, a2, a3, a4, and a5 are constant symbols in L6F(X), then Sσ = {P(a1), (P(a1)→ d) ∨ (Z1(a1) ↔ Q(a2)), (Z1(a1) ↔ Q(a2))′ ∨ (T(a3) → d), Z(a4) → T(a3), (Z(a4) → Z1(a5))′}, and Sσ ≤ d, then there exists a non-clausal multi-ray α -generalized resolution refutation ω0 from Sσ in L6P(X) as follows:

  1. (1)

    P(a1)

  2. (2)

    (P(a1)→ d) ∨ (Z1(a1) ↔ Q(a2))

  3. (3)

    (Z1(a1) ↔ Q(a2))′ ∨ (T(a3) → d)

  4. (4)

    Z(a4) → T(a3)

  5. (5)

    (Z(a4) → Z1(a5))′

    -------------------------------

  6. (6)

    d ∨ (Z1(a1) ↔ Q(a2))   by (1), (2)

    -------------------------------

  7. (7)

    d ∨ (T(a3) → d)    by (3), (6)

    -------------------------------

  8. (8)

    d-□ by (4), (5), (7)

By Lifting Lemma of non-clausal multi-ray α-generalized resolution, there exists a non-clausal multi-ray α-generalized resolution refutation ω from S in L6F(X) similar to Example 4.1. Therefore, the non-clausal multi-ray α-generalized resolution refutation ω of S is:

  • P(a1),

  • (P(a1)→ d) ∨ (Z1(w) ↔ Q(y)),

  • (Z1(w) ↔ Q(y))′ ∨ (T(a3) → d),

  • Z(a4) → T(a3),

  • (Z(a4) → Z1(a5))′,

  • d ∨ Q(y),

  • d ∨ (T(z) → d),

  • d-□.

Furthermore, if we judge the α-unsatisfiability of S by α-resolution principle, we firstly transform S to its generalized conjunctive normal form S1 = {P(x), (P(x)→d) ∨(Z1(w) → Q(y)), (P(x)→ d) ∨(Q(y) → Z1(w)), (Z1(w) → Q(y))′ ∨ (Q(y) → Z1(w))′ ∨ (T(z) → d), Z(t) → T(z), (Z(t) → Z1(u))′}.

Then we take a ground substitution σ ={a1 / x, a2 / y, a3 / z, a4 / t, a5 / u, a1 / w} of S, then S1σ = {P(a1), (P(a1)→ d)∨(Z1(a1) → Q(a2)), (P(a1)→ d) ∨ (Q(a2) → Z1(a1)), (Z1(a1) → Q(a2))′ ∨ (Q(a2) → Z1(a1))′ ∨ (T(a3) → d), Z(a4) → T(a3), (Z(a4) → Z1(a5))′}, and S1σ ∨≤ d, then we cannot get a binary α-resolution refutation of S1σ, but can get a relatively complex multi-ray α-resolution refutation of S1σ [24], i.e., there exists a multi-ray α-resolution refutation ω0 from S1σ in L6F(X) as follows:

  1. (1)

    P(a1)

  2. (2)

    (P(a1)→ d)∨(Z1(a1) → Q(a2))

  3. (3)

    (P(a1)→ d) ∨ (Q(a2) → Z1(a1))

  4. (4)

    (Z1(a1)→Q(a2))′∨(Q(a2)→Z1(a1))′∨(T(a3)→d)

  5. (5)

    Z(a4) → T(a3)

  6. (6)

    (Z(a4) → Z1(a5))′

    -------------------------------

  7. (7)

    d ∨ (Z1(a1) → Q(a2))   by (1), (2)

  8. (8)

    d ∨ (Q(a2) → Z1(a1))   by (1), (3)

    -------------------------------

  9. (9)

    d∨(Q(a2)→ Z1(a1))′ ∨ (T(a3)→d)  by (4), (7)

    -------------------------------

  10. (10)

    d ∨ (T(a3) → d)    by (8), (9)

    -------------------------------

  11. (11)

    d-□     by (5), (6), (10)

Similarly, by Lifting Lemma of multi-ray α-resolution, there exists a multi-ray α-resolution refutation ω from S1 in L6F(X), that is, we resume the variable symbols in S1 which are substituted by σ in S1σ. Therefore, the multi-ray α-resolution refutation ω of S1 is:

  • P(x),

  • (P(x)→ d) ∨(Z1(w) → Q(y)),

  • (P(x)→ d) ∨(Q(y) → Z1(w)),

  • (Z1(w) → Q(y))′ ∨ (Q(y) → Z1(w))′ ∨ (T(z) → d),

  • Z(t) → T(z),

  • (Z(t) → Z1(u))′

  • d ∨ (Z1(w) → Q(y)),

  • d ∨ (Q(y) → Z1(w)),

  • d ∨ (Q(y) → Z1(w))′ ∨ (T(z) → d),

  • d ∨ (T(z) → d),

  • d-□.

Theorem 4.8 and Theorem 4.9 show that the non-clausal multi-ray α-generalized resolution deduction in LF(X) is sound and complete, along with Examples 4.1 and 4.2 to illustrate its advantages in terms of reasoning capability and efficiency. Similarly in LP(X), Examples 4.1 and 4.2 show that for an α -unsatisfiable set of general g-clause in LF(X), if we convert it into respectively generalized conjunctive normal form, and judge it by α-resolution principle, then it may not lead to a binary α-resolution refutation partially because its restriction of the number of α -resloved literals is 2. Although sometimes it may lead to a multi-ray α-resolution refutation, but it is more complex than the non-clausal multi-ray α-resolution refutation.

Consequently, the proposed work is a great extension of the results in [24–26] in terms of soundness and completeness, applicability, reasoning capability and reasoning efficiency.

Remark 4.2.

In fact, it follows from Theorem 4.5 that the determination of α-generalized resolution in LF(X) can be equivalently transformed into that of α -generalized resolution in LP(X) to some extents, which reduces the difficulty of α -generalized resolution in LF(X) to some extents. Hence, the determination of α -generalized resolution in LP(X) would be the next key step for developing efficient α-resolution reasoning algorithm for LP(X) as well as LF(X). However, similar to the one indicated in [24], the practical implementations of a resolution deduction algorithm are much more complex, especially in the case of first-order logic. It can be tracked back to 1931 when Godel proposed the famous undecidability theory, that is, it is impossible to construct a single algorithm that can always lead to a correct true-or-false answer for all logical formulae in a specified deductive system.

The focus of this paper is on the resolution principle and the theoretical soundness and completeness of this resolution-based automated deduction, not on the concrete algorithms or search strategies for implementation. For resolution-based automated reasoning in lattice-valued logic based on LIE, 1) it is more complex than that in classical logic from the logical point of view; 2) it will be not that straightforward either in determining or search which group of generalized literals could be α -resoluble, that is, resoluble at a truth-value level α, or determining at least how many generalized literals can be chosen in the α -resolution group once given a truth-value level α; 3) although the resolution process can borrow the similar ideas from classical logic, it becomes more complex due to the more complex generalized literals involved in the resolution and also the fact that it allows the choice of various truth-value level resolution (different from the only case of α=O in classical logic).

Consequently, it is much harder or more computationally complex to achieve the α-resolution-based automated reasoning algorithm in lattice-valued logic based on LIE than to achieve it in the classical logic. This kind of concrete algorithms or search strategies for implementation will be still one of challenge problems in α-resolution-based automated reasoning in lattice-valued logic based on LIE, will need more efforts to investigate in the future, this topic, however, is beyond the scope of the present work.

5. Related works

Lattice-valued logics as ones of the most important many-valued logics, extend the chain-type truth-valued field to a general lattice structure in which the truth-values are incompletely comparable with each other [23, 34–43]. Lattice-valued logics are thus an important and promising research direction that provides an alternative logical approach to dealing with imprecision and incomparability as well [23].

Up to now, many researchers have made investigation on resolution-based automated reasoning in the framework of fuzzy logic and many-valued logics, and obtained some important results [38, 42, 44–80].

Aiming at establishing automated deduction for many-valued logic, Xu et al. introduced a binary resolution at a certain truth-value level α (called α -resolution principle) and developed the α-resolution deduction in a lattice-valued logic L(X) based on a lattice-valued logic algebra – lattice implication algebra (LIE) and proved its soundness and completeness [25, 26]. Compared with the resolution principle in Boolean logic, the α-resolution principle in lattice-valued logic L(X) has new features such as: (a) α -resolution is proceeded at different truth-value level α (with the possible incomparability) chosen from the truth-valued field – LIE; (b) α -resolution is based on generalized literals, which contain constant formula and more general implication connective than the one in the classical logic. Hence the expressive power is enhanced. Actually, implication connectives in L(X) are not reducible to other classical logical connectives, which is different from the Kleene implication (i.e., p → q = p′ ∨ q). This International Journal of Computational Intelligence Systems, irreducibility is semantically meaningful, complicates the calculus; (c) judging whether two generalized literals are α -resolvable should consider both semantic and syntax consistently [25, 26].

Although LIAs have been investigated independently, it has been proved [23] that LIAs are categorically equivalent to (i.e., coincide with) the class of MV algebra, which are the algebraic semantics of Łukasiewicz logic. LIAs form a variety of algebras and the variety of LIE-algebras contains all Boolean algebras and Łukasiewicz algebra (i.e., the variety of algebras of Lukasiewicz logic), two of the most commonly investigated logic algebra in classical logic and many-valued logic. The focus of the present paper is establishing a sound and complete resolution-based reasoning system based on LIAs, which 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 L(X) based on LIE in several ways have extended and expanded Pavelka fuzzy logic [23, 36]. This shows that the investigation of resolution-based automated reasoning for L(X) 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 (where these ideas can be applied in some other relevant logic systems based on different logic semantic algebras). This reflects the key motivation for the proposed work.

Although there has been some research work on resolution-based automated reasoning methods based on non-classical logic (e.g., for fuzzy logic and many-valued logic) as cited earlier, 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, because there is no constant formula involved in the syntax of the logic system so they have the syntactical equivalence, this is one of the key differences form the automated deduction in signed logic or annotated logic [20, 44, 56, 57, 81, 82], Bilattice-based logics [83], probabilistic logic [84], similarity-based logic [85]. The works related to Lukasiewicz logic have been mainly focused on generalized CNF based on bold product and bold sum operators or logic programming [59, 76, 77]. As far as we know, proof theory for lattice-valued logic has so far not been extensively developed.

6. Conclusions

In this paper, a non-clausal multi-ray α-generalized resolution principle and its resolution deduction for lattice-valued logic based on a lattice-valued logical algebra - LIE were proposed. The definitions of the general form of non-clausal multi-ray α -generalized resolution and non-clausal multi-ray α -generalized resolution deduction in LP(X) were given, along with its soundness and completeness. In order to obtain the completeness of this general form of non-clausal multi-ray α -generalized resolution principle in LF(X), the α -unsatisfiability of the general form of logical formula was discussed. Finally, by Lifting Lemma and the completeness of the ground case, the completeness of the general case was obtained. This contribution is expected to provide a theoretical foundation for more efficient and effective resolution based automated reasoning algorithms and tools in lattice-valued logic with the goal of applying them to some practical fields such as expert system design, intelligent robot design, and machine learning system design under uncertain environment. The further research will be concentrated on contriving an algorithm to achieve the efficiency of the non-clausal multi-ray α -generalized resolution, and investigating the non-clausal multi-ray α -generalized resolution in linguistic truth-valued lattice-valued logic[86] for some applications.

Acknowledgments

This work is supported by the National Science Foundation of China (Grant No. 61673320) and the Fundamental Research Funds for the Central Universities (Grant No. 2682017ZT12).

References

2.Johan van Benthem and Alice ter Meulen, Handbook of Logic and Language, 2rd edition, Elsevier, 2010.
5.D Plaisted, History and prospects for first-order automated deduction, in Proceedings of the 25th International Conference on Automated Deduction (Berlin, Germany, August 1–7 2015), pp. 3-28.
6.SH Muggleton, Alan Turing and the development of Artificial Intelligence, AI communications, 2013. forthcoming,
13.C Green, The application of theorem proving to question-answering systems, Stanford University, Stanford, 1969. Ph.D. thesis,
14.U Furbach, I Glöckner, and B Pelzer, An application of automated reasoning in natural language question answering, AI Communications, Vol. 23, No. 2–3, 2010, pp. 241-265.
16.XH Wang and XH Liu, Generalized resolution, Chinese journal of computers, Vol. 2, 1982, pp. 81-92. (in Chinese).
17.Z Stachniak, Resolution Proof Systems: An Algebraic Theory, Kluwer Academic Publisher, Netherlands, 1996.
18.Z Stachniak, Non-Clausal Reasoning with Definite Theories, Fundamenta Informaticae, Vol. 48, 2001, pp. 1-26.
20.R Hahnle, Automated deduction in multiple-valued logics, Oxford University Press, Inc, 1993.
21.H Habiballa, Non-clausal resolution - theory and practice. Research report, University of Ostrava, 2000.
22.Y Xu, Lattice implication algebras, J. Southwest Jiaotong University, Vol. 89, No. 1, 1993, pp. 20-27. (in Chinese).
29.Y Xu, J Liu, XX He, XM Zhong, and SW Chen, Non-clausal multi-ray α-generalized resolution principle for a lattice-valued propositional logic, in Proceeding of the 11th International FLINS Conference on Decision Making and Soft Computing (FLINS2014)/9th International Conference on Intelligent Systems and Knowledge Engineering (ISKE 2014) (Joao Pessoa, Brazil, August 17–20, 2014), pp. 197-202.
37.S Gottwald, A Treatise on Many-Valued Logics. Studies in Logic and Computation, Vol. 9, Research Studies Press Ltd, Baldock, 2001.
39.V Novak, Fuzzy Sets and Their Applications, Adam Hilger, Bristol, 1989.
43.G Birkhoff, Lattice Theory, 3rd edition, American Mathematical Society, Providence, R.L, 1967.
53.C Ansótegui, M Bofill, F Manyà, and M Villaret, SAT and SMT technology for many-valued logics, Journal of Multiple-Valued Logic & Soft Computing, Vol. 24, No. 1–4, 2015, pp. 151-172.
55.XH Liu, Resolution-Based Automated Reasoning, Academic Press, Beijing, China, 1994. (in Chinese)
72.XM Zhong and Y Xu, alpha- group quasi-lock semantic resolution method based on lattice-valued propositional logic LP(X), Multiple-Valued Logic and Soft Computing, Vol. 22, No. 4–6, 2014, pp. 581-598.
76.V Sofronie-Stokkermans, Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators, Multiple-Valued Logic–An International Journal, Vol. 6, No. 3–4, 2001, pp. 289-344.
77.V Sofronie-Stokkermans and C Ihlemann, Automated reasoning in some local extensions of ordered structures, Journal of Multiple-Valued Logic and Soft Computing, Vol. 13, No. 4–6, 2007, pp. 397-414.
84.F Bacchus, Representing and Reasoning with Probabilistic Knowledge: A Logical Approach to Probabilities, MIT Press, Cambridge, MA, USA, 1991.
<Previous Article In Issue
Download article (PDF)
Next Article In Issue>
Journal
International Journal of Computational Intelligence Systems
Volume-Issue
11 - 1
Pages
384 - 401
Publication Date
2018/01/01
ISSN (Online)
1875-6883
ISSN (Print)
1875-6891
DOI
10.2991/ijcis.11.1.29How to use a DOI?
Copyright
© 2018, the Authors. Published by Atlantis Press.
Open Access
This is an open access article under the CC BY-NC license (http://creativecommons.org/licences/by-nc/4.0/).

Cite this article

risenwbib
TY  - JOUR
AU  - Yang Xu
AU  - Jun Liu
AU  - Xingxing He
AU  - Xiaomei Zhong
AU  - Shuwei Chen
PY  - 2018
DA  - 2018/01/01
TI  - Non-Clausal Multi-ary α-Generalized Resolution Calculus for a Finite Lattice-Valued Logic
JO  - International Journal of Computational Intelligence Systems
SP  - 384
EP  - 401
VL  - 11
IS  - 1
SN  - 1875-6883
UR  - https://doi.org/10.2991/ijcis.11.1.29
DO  - 10.2991/ijcis.11.1.29
ID  - Xu2018
ER  -