Elsevier

Information Sciences

Volume 130, Issues 1–4, December 2000, Pages 195-223
Information Sciences

α-Resolution principle based on lattice-valued propositional logic LP(X)

https://doi.org/10.1016/S0020-0255(00)00069-4Get rights and content

Abstract

In the present paper, resolution-based automated reasoning theory in an L-type fuzzy logic is focused. Concretely, the α-resolution principle, which is based on lattice-valued propositional logic LP(X) with truth-value in a logical algebra – lattice implication algebra, is investigated. Finally, an α-resolution principle that can be used to judge if a lattice-valued logical formula in LP(X) is always false at a truth-valued level α (i.e., α-false), is established, and the theorems of both soundness and completeness of this α-resolution principle are also proved. This will become the theoretical foundation for automated reasoning based on lattice-valued logical LP(X).

Introduction

Since its introduction in 1965, automated reasoning based on Robinson's [12] resolution rule has been extensively studied [13], [16], [19] in the context of finding natural and efficient proof systems to support a wide spectrum of computational tasks. A number of important applications of such systems have been found in areas such as artificial intelligence, logic programming, problem solving and question answering systems, database theory, and so on. As the real world is dealing with uncertainty, it is difficult to design any intelligent system based on traditional logic. In other words, any intelligent system that is designed to work in this real world must be able to make “decisions” in a fuzzy environment. With the development of Zadeh's [6] fuzzy logic, expert systems and knowledge engineering, especially since non-classical logics became a considerable formal tool for computer science and artificial intelligence, the area of automated reasoning based on non-classical logic (especially multi-valued logic and fuzzy logic) has drawn the attention of many researchers.

The first step in automated deduction in fuzzy logic was made by Lee and Chang [17] and Lee [18]. Many subsequent works were based on Lee's definitions and results. Mukaidono [20], [21] generalized Lee's results by introducing a fuzzy resolvent. Yager [22] independently proposed a multi-valued propositional logic system similar to Lee's fuzzy logic system, with a notion of logical consequence stronger than Lee's. He generalized resolution in the same spirit as Mukaidono's. Lee's fuzzy formulae are syntactically defined exactly as classical first-order formulae, the only difference between them being the value of the atom, i.e., they differ semantically. Therefore, these fuzzy logics cannot describe fuzzy reasoning completely. In 1985, Liu and Xiao [23], [24], [25], [27] proposed an operator fuzzy logic system, which is able to represent the fuzzy-degree of a fuzzy proposition. Although these works implemented and extended the classical resolution principle, the choice of their implication connective was limited to Kleene implication (i.e., pqpq). This fact leads to the syntactical equivalence of the language with the classical first-order logic. Hence, these fuzzy logic systems have a common feature, i.e., a clause set S is unsatisfiable in fuzzy logic if and only if S is unsatisfiable in the classical logic. Orlowska and Wierzchon [26] introduced a deduction system based on decomposition rules, for a fuzzy logic with the classical language, Gödel's implication and an intuitionistic negation. The deduction system can prove that a formula is a tautology. Dubois and Prade proposed a resolution principle in possibilistic logic [28], [29], [30].

In the framework of multi-valued logic [3], [4], [5], [10], [11], perhaps the earliest reference to a multi-valued resolution-based deduction system is the one proposed by Morgan [31]. Afterwards, Orlowska [32], [33], [34] proposed an automated reasoning theory and an application in ω+-valued logic and in post's finite-valued logic. Schmitt [35] proposed a resolution-based proof system for a certain three-valued logic. Recently, a general treatment of resolution for multi-valued logic based on signed clauses has been published. One feature common to much of these works is the use of signs (subsets of the set of truth-values). This method was independently proposed by Hahnle [36], [37], [38], [39], Murray and Rosenthal [40], [41]. Other authors, such as Blair and Subrahamanian [42], da Costa et al. [43], Kifer et al. [44], Subrahamanian [45], Kifer and Lozinski [46], Kifer and Subrahamanian [47] Baaz et al. [56] and Lu and Henschen [48], studied the annotated logic system. It has been proved that the annotated-logic and operator fuzzy logic are special cases of the signed logic [49], [50]. Multi-valued logic may lack the expressive power to allow normal form. Not even a disjunctive operator needs to be present. One way to deal with this situation is to embody the multi-valued version of non-classical resolution system as it has been presented for classical logic [14], [15], [51]. An example of a multi-valued logic system, which can deal with this issue is Stachniak's resolution-based proof system [52], [53], [54], [55]. To summarize, Stachniak's resolution-based approach to theorem proving in multi-valued logic is of considerable flexibility and covers a wide scope of logic.

Multi-valued logic is an extension and a development of classical logic. Its truth-value field and logical rule has more power to express human thinking and the real world. From the logical viewpoint, fuzzy logic can be regarded as a kind of multi-valued or infinite-valued logic.

Lattice-valued logic is an important case of multi-valued logic. A lattice [1] is a kind of important algebraic structure that is an abstract model of the real world. Lattice-valued logic extends the chain-type truth-valued field to a general lattice, which can more efficiently model the uncertainty of human thinking, judgement and decision. Up to now, the study of lattice-valued logic is not complete, especially for complex truth-value fields with incomparable information as well as for the corresponding proof system and automated reasoning.

To establish a logic system with truth values in a relatively general lattice, in 1990, during the study of the project “The Study of Abstract Fuzzy Logic” granted by National Nature Science Foundation, we firstly established the lattice implication algebra [57] by combining lattice and implication algebra, and investigated many of its structures [57], [58], [59], [60], [61], [62], [63], [64], [65], [66], [67], [68], [69], [70], [71], [72], [73] and this became the foundation for establishing the corresponding logic system from an algebraic point of view. We have also established several lattice-valued logic systems [74], [75], [76], [77], [78], [79], [80], [81], [82], [83], [84], [85]. In [74], [75], we proposed a lattice-valued propositional logic algebra LP(X) based on lattice implication algebra. Moreover, we proposed the more general form of lattice-valued propositional logic LP(X) in [81], [82]. In [76], [77], we established a first-order lattice-valued logic system FM based on L-type lattice-valued propositional logic LP(X). As an application of LP(X), we established a fuzzy propositional logic FP(X) based on the Lukasiewicz implication operator in [78] as well as a fuzzy-valued propositional logic FP*(X) in [79].

It is well known that the difference of degree among attributes of each intermediate variation state of things brings out the uncertainty of things, especially the fuzziness of things. Henceforth, to establish a logic system that can efficiently characterize this kind of uncertainty, we need to gradually express this difference of degree and to establish a dynamic lattice-valued logic system that can be sufficient to reflect dynamically a gradual technique instead of a static one. Based on Goguen [7], Pavelka [8] and Novak's [9] works as well as on ours, we further studied the gradual L-type lattice-valued logic system Lvl based on lattice implication algebra. In 1997, we established an gradual L-type lattice-valued propositional logic Lvpl [83] related to a truth-value degree, and established the corresponding gradual L-type first-order lattice-valued logic system Lvfl [84], [85] related to a truth-value degree. Moreover, we investigated the approximate reasoning methods and the resolution-based automated reasoning based on the established lattice-valued logic systems [86], [87], [88], [89], [90].

In this paper, we will establish a resolution-based proof theory for the lattice-valued logic LP(X) [81], [82] based on the ideas expressed in the following principles:

1. The extension of a truth-value field from {0,1} to a lattice, i.e., the lattice implication algebra. In the real world, various uncertain pieces of information may be comparable or incomparable. To establish the automated reasoning methods to deal with both total ordering (i.e., that may be comparable) information and non-total ordering information (i.e., incomparable), it is necessary and important to investigate a non-classical logical system with the corresponding characteristics. Since a lattice is an algebraic abstract of the real world, it can be used to model uncertain information that may be comparable or not comparable. Lattice-valued logic is an important and promising research direction.

2. The extension of implication connectives. It is well known that several implication connectives, which formalize different nuances of multi-valued logics, have been introduced and used. Multi-valued logic systems with different implication operations capture different aspects of vagueness (imprecision, approximation, etc.) present in the description of the state of affairs. As we mentioned previously, the choice of Kleene's implication will lead to the syntactical equivalence of language with the classical logic [2]. Therefore, the choice of more general implication connectives and their application in fuzzy logic, especially their possible integration with resolution-based automated reasoning, is desirable. Since lattice-valued logics with truth-value in lattice implication algebras are a great extension in several aspects such as connectives, truth-valued field and inference rules. Especially the implication connectives are more general and not reducible to the other classical connectives, unlike Kleene's. This irreducibility, though semantically justifiable, complicates the calculus. As a first step towards a variant resolution, it is important to deal with implication connectives.

3. Semantic issues. It is well known that the management of truth-values is a central issue in multi-valued logics in general, and in the particular use which is made of them as a technical tool for modelling approximate reasoning. In using multi-valued logic as a tool for the modelling of approximate reasoning, it is also important to have some sorts of control on the truth-value assumed by the conclusion, once the truth-values of the premises are given. This is not the case of classical logic of which the semantics are too easy to be considered especially during the resolution deduction instead of being characterized only by syntactical concepts. Hence, we should consider the consistency between syntax and semantics to model approximate reasoning. Therefore, the resolution principle should be involved in both syntax and semantics, and some truth-value level of resolution. It is also very important to establish the completeness theorems.

According to the above remarks, this paper will extend the resolution principle based upon reductio ad absurdum from binary logic into lattice-valued logic. Concretely, we will establish a lattice-valued resolution principle based on a lattice-valued propositional logic system LP(X) with truth-value in a logical algebraic structure – lattice implication algebras. In this paper, we shall firstly introduce some important concepts and results about lattice implication algebras and lattice-valued logic system LP(X). Then we shall interpret the concept of lattice-valued resolvent. Subsequently, we shall consider the lattice-valued resolution principle. Finally, we will prove the soundness and completeness of this resolution principle, which will become a foundation for constructing automated reasoning methods to deal with uncertain information both comparable and incomparable.

Section snippets

Preliminaries

We have studied many properties about lattice implication algebras and lattice-valued propositional logic LP(X). Here, we will give only some elementary concepts, the details can be seen in the related Refs. [57], [58], [59], [60], [61], [62], [63], [64], [65], [66], [67], [68], [69], [70], [71], [72], [73], [74], [75], [76], [81], [82].

Definition 2.1

[57]. Let (L,∨,∧,O,I) be a bounded lattice with order-reversing involution `', →:L×LL be a mapping. (L,∨,∧,,→) is called a lattice implication algebra if the

α-Resolution principle based on LP(X)

Beginning from the normal form is the natural and usual way to discuss the validity and satisfiability of the formula in classical logic. Considering the great extension in connectives and truth-values in LP(X). Especially the implication connectives in LP(X) are more general and not reducible to the other classical connectives, unlike Kleene's. This irreducibility, though semantically justifiable, complicates the calculus. As a first step towards a variant resolution, it is important to deal

Soundness and completeness

Since the semantic structure is much more important in multi-valued logic systems compared with the classical logic system, the resolution principle should be involved in both syntax and semantics and we should consider the consistency between syntax and semantics. Hence, it is also very important to establish the soundness and the completeness theorems.

Theorem 4.1 Soundness theorem

Suppose a generalized conjunctive normal form S=C1∧C2∧⋯∧Cn,α∈L,{D1,D2,…,Dm} is an α-resolution deduction from S to a generalized clause Dm.

If Dm

Conclusion

Since a lattice is an algebraic abstract of the real world, it can be used to model uncertain information that may be comparable or incomparable. Lattice-valued logic is an important and promising research direction. Based on our previous works about the lattice-valued logical algebra and lattice-valued logics as well as other related works, we extend the resolution principle based upon reductio ad absurdum from binary logic into lattice-valued logic. Concretely, the α-resolution principle,

Acknowledgements

The authors express their sincere thanks to the referees for their valuable comments and suggestions, which have helped the presentation.

References (90)

  • L. Bolc et al.

    Many-Valued Logics

    (1992)
  • J.B. Rosser et al.

    Many-Valued Logic

    (1952)
  • N. Rescher

    Many-Valued Logic

    (1969)
  • J.A. Goguen

    The logic of inexact concepts

    Synthese

    (1969)
  • J. Pavelka, On fuzzy logic I: Many-valued rules of inference, II: Enriched residuated lattices and semantics of...
  • V. Novak

    First-order fuzzy logic

    Studia Logica

    (1982)
  • D. Dubois, H. Prade, The generalized modus ponens under sup-min composition – A theoretical study, in: M.M. Gupta et...
  • D. Dubois, J. Lang, H. Prade, Fuzzy sets in approximate reasoning, Part I: Inference with possibility distributions,...
  • J.P. Robinson

    A machine-oriented logic based on the resolution principle

    J. ACM

    (1965)
  • D.W. Loveland

    Automated Theorem Proving: A Logical Basis

    (1978)
  • X.H. Wang, X.H. Liu, Generalized resolution, J. Comput. (2) (1982) 81–92 (in...
  • L. Wos

    Automated Reasoning: Basic Research Problems

    (1988)
  • R.C.T. Lee

    Fuzzy logic and the resolution principle

    J. ACM

    (1972)
  • C.L. Chang et al.

    Symbolic Logic and Mechanical Theorem Proving

    (1973)
  • M. Mukaidono

    On some properties of fuzzy logic

    Syst. Comput. Control

    (1975)
  • M. Mukaidono

    Fuzzy inference of resolution style

  • X.H. Liu, H. Xiao, Operator fuzzy logic and fuzzy resolution, in: Proceedings of the Fifth IEEE International Symposium...
  • T.J. Weigert et al.

    Fuzzy operator logic and fuzzy resolution

    J. Autom. Reasoning

    (1993)
  • X.H. Liu

    Resolution-based Automated Reasoning

    (1994)
  • E. Orlowska et al.

    Mechanical reasoning in fuzzy logics

    Logique et Analyses

    (1985)
  • X.H. Liu, Fuzzy Logic and Fuzzy Reasoning, Press of Ji Lin University, 1989 (in...
  • D. Dubois, J. Lang, H. Prade, Theorem proving under uncertainty – A possibility theory based approach, in: Proceedings...
  • D. Dubois, J. Lang, H. Prade, Automated reasoning using possibility logic semantics, belief revision and variable...
  • C.G. Morgan

    Resolution for many-valued logics

    Logique et Analyses

    (1976)
  • E. Orlowska

    The resolution principle for ω+-valued logic

    Fundamenta Informaticae

    (1978)
  • E. Orlowska

    Resolution system and their application II

    Fundamenta Informaticae

    (1980)
  • E. Orlowska

    Mechanical proof methods for Post logics

    Logique et Analyses

    (1985)
  • P.H. Schmitt

    Computational aspects of three-valued logic

  • R. Hahnle, Uniform notation tableau rules for multiple-valued logics, in: Proceedings of the International Symposium on...
  • R. Hahnle, Towards an efficient tableau proof procedure for multiple-valued logics, in: Proceedings of the Workshop on...
  • R. Hahnle

    Automated Deduction in Multiple-Valued Logics

    (1993)
  • R. Hahnle, Short CNF in finitely-valued logics, in: J. Komorowski, Z.W. Ras (Eds.), in: Proceedings of the Seventh...
  • N.V. Murray, E. Rosenthal, Resolution and path dissolution in multiple-valued logics, in: Proceedings of the Sixth...
  • N.V. Murray, E. Rosenthal, Improving tableau proof in multiple-valued logic, in: Proceedings of the 21st International...
  • N.C.A. da Costa et al., Automated theorem proving in paraconsistent logics: theory and implementation, in: W....
  • Cited by (126)

    View all citing articles on Scopus

    The work was supported by the Project of Flanders-China cooperation (1999) and the National Natural Science Foundation of People's Republic of China with Grant No. 69674015 and 69774016.

    1

    Tel.: +32-14-33-22-72; fax: +32-14-32-15-29.

    View full text