Title :
A resolution-like strategy based on a lattice-valued logic
Author :
Liu, Jun ; Ruan, Da ; Xu, Yang ; Song, Zhenming
Author_Institution :
Dept. of Appl. Math., Southwest Jiaotong Univ., Chengdu, China
Abstract :
As the use of nonclassical logics becomes increasingly important in computer science, artificial intelligence and logic programming, the development of efficient automated theorem proving based on nonclassical logic is currently an active area of research. This paper aims at the resolution principle for the Pavelka type fuzzy logic (1979). Pavelka showed that the only natural way of formalizing fuzzy logic for truth-values in the unit interval [0, 1] is by using the Lukasiewicz´s implication operator a→b=min{1,1-a+b} or some isomorphic forms of it. Hence, we first focus on the resolution principle for the Lukasiewicz logic Lℵ with [0, 1] as the truth-valued set. Some limitations of classical resolution and resolution procedures for fuzzy logic with Kleene implication are analyzed. Then some preliminary ideals about combining resolution procedure with the implication connectives in Lℵ are given. Moreover, a resolution-like principle in Lℵ is proposed and the soundness theorem of this resolution procedure is also proved. Second, we use this resolution-like principle to Horn clauses with truth-values in an enriched residuated lattice and consider the L-type fuzzy Prolog.
Keywords :
formal logic; fuzzy logic; theorem proving; AI; Pavelka type fuzzy logic; artificial intelligence; computer science; efficient automated theorem proving; lattice-valued logic; logic programming; nonclassical logics; resolution-like strategy; Artificial intelligence; Computer science; Expert systems; Fuzzy logic; Knowledge engineering; Lattices; Logic programming; Mathematics; Proposals;
Journal_Title :
Fuzzy Systems, IEEE Transactions on
DOI :
10.1109/TFUZZ.2003.814859