DocumentCode :
763006
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
Volume :
11
Issue :
4
fYear :
2003
Firstpage :
560
Lastpage :
567
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;
fLanguage :
English
Journal_Title :
Fuzzy Systems, IEEE Transactions on
Publisher :
ieee
ISSN :
1063-6706
Type :
jour
DOI :
10.1109/TFUZZ.2003.814859
Filename :
1220301
Link To Document :
بازگشت