On α-satisfiability and its α-lock resolution in a finite lattice-valued propositional logic

Xingxing He, Jun Liu, Yang Xu, Luis Martínez, Da Ruan

    Research outputpeer-review

    Abstract

    Automated reasoning issues are addressed for a finite lattice-valued propositional logic LnP(X) with truth-values in a finite lattice-valued logical algebraic structure-lattice implication algebra. We investigate extended strategies and rules from classical logic to LnP(X) to simplify the procedure in the semantic level for testing the satisfiability of formulas in LnP(X) at a certain truth-value level α (α-satisfiability) while keeping the role of truth constant formula played in LnP(X). We propose a lock resolution method at a certain truth-value level α (α-lock resolution) in LnP(X) and have proved its theorems of soundness and weak completeness, respectively. We provide more efficient resolution based automated reasoning in LnP(X) and key supports for α-resolution-based automated reasoning approaches and algorithms in lattice based linguistic truth-valued logic.

    Original languageEnglish
    Pages (from-to)579-588
    Number of pages10
    JournalLogic Journal of the IGPL
    Volume20
    Issue number3
    DOIs
    StatePublished - Jun 2012

    Funding

    National Natural Science Foundation of China (Grant No. 60875034) and the research project (TIN-2006-02121 and P08-TIC-3548) (in part).

    FundersFunder number
    NSFC - National Natural Science Foundation of ChinaP08-TIC-3548, TIN-2006-02121, 60875034

      ASJC Scopus subject areas

      • Logic

      Cite this