A resolution-like strategy based on a lattice-valued logic

Jun Liu, Da Ruan, Yang Xu, Zhenming Song

    Research outputpeer-review

    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 languageEnglish
    Pages (from-to)560-567
    Number of pages8
    JournalIEEE Transactions on Fuzzy Systems
    Volume11
    Issue number4
    DOIs
    StatePublished - Aug 2003

    ASJC Scopus subject areas

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

    Cite this