## 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. Pavelka showed (in 1979) that the only natural way of formalizing fuzzy logic for truth-values in the unit interval [0, 1] is by using the Łukasiewicz'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 Łukasiewicz 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.

Original language | English |
---|---|

Pages (from-to) | 560-567 |

Number of pages | 8 |

Journal | IEEE Transactions on Fuzzy Systems |

Volume | 11 |

Issue number | 4 |

DOIs | |

State | Published - Aug 2003 |

## ASJC Scopus subject areas

- Control and Systems Engineering
- Computational Theory and Mathematics
- Artificial Intelligence
- Applied Mathematics