α-Resolution principle based on lattice-valued propositional logic 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., p→q=¬p∨q). 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×L→L 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 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)
Fuzzy sets
Information and Control
(1965)Completely non-clausal theorem proving
Artificial Intelligence
(1982)- et al.
Some properties of fuzzy logic
Information and Control
(1971) Inference in a multiple-valued logic system
Int. J. Man Machine Stud.
(1985)- et al.
Resolution principle in possibilistic logic
Int. J. Approx. Reasoning
(1990) - et al.
Paraconsistent logic programming
Theoret. Comput. Sci.
(1989) - et al.
Theory of generalized annotated logic programming and its application
J. Logic Programming
(1992) - et al.
The completeness of gp-resolution for annotated logic
Inform. Process. Lett.
(1992) Lattice Theory
(1967)- et al.
An Algebraic Introduction to Mathematical Logic
(1975)
Many-Valued Logics
Many-Valued Logic
Many-Valued Logic
The logic of inexact concepts
Synthese
First-order fuzzy logic
Studia Logica
A machine-oriented logic based on the resolution principle
J. ACM
Automated Theorem Proving: A Logical Basis
Automated Reasoning: Basic Research Problems
Fuzzy logic and the resolution principle
J. ACM
Symbolic Logic and Mechanical Theorem Proving
On some properties of fuzzy logic
Syst. Comput. Control
Fuzzy inference of resolution style
Fuzzy operator logic and fuzzy resolution
J. Autom. Reasoning
Resolution-based Automated Reasoning
Mechanical reasoning in fuzzy logics
Logique et Analyses
Resolution for many-valued logics
Logique et Analyses
The resolution principle for ω+-valued logic
Fundamenta Informaticae
Resolution system and their application II
Fundamenta Informaticae
Mechanical proof methods for Post logics
Logique et Analyses
Computational aspects of three-valued logic
Automated Deduction in Multiple-Valued Logics
Cited by (126)
(α, β)-Ordered linear resolution of intuitionistic fuzzy propositional logic
2017, Information SciencesChinese Research on Mathematical Logic and the Foundations of Mathematics
2022, Asian StudiesA Topology Graph Algorithm Based on Lattice-Valued Logic to Solve Satisfiability Problems
2022, Mathematical Problems in EngineeringDetermination of 3-ary α-resolution in LP(X)
2021, 2021 IEEE International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2021Non-clausal multi-ary α-generalized resolution calculus for a finite lattice-valued logic
2018, International Journal of Computational Intelligence Systems
- ☆
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.