α-satisfiability and α-lock resolution for a lattice-valued logic LP(X)

Xingxing He, Yang Xu, Yingfang Li, Jun Liu, Luis Martinez, Da Ruan

    Research output: Contribution to journalConference articlepeer-review

    8 Citations (Scopus)

    Abstract

    This paper focuses on some automated reasoning issues for a kind of lattice-valued logic LP(X) based on lattice-valued algebra. Firstly some extended strategies from classical logic to LP(X) are investigated in order to verify the α-satisfiability of formulae in LP(X) while the main focus is given on the role of constant formula played in LP(X) in order to simply the verification procedure in the semantic level. Then, an α-lock resolution method in LP(X) is proposed and the weak completeness of this method is proved. The work will provide a support for the more efficient resolution based automated reasoning in LP(X).

    Original languageEnglish
    Pages (from-to)320-327
    Number of pages8
    JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume6077 LNAI
    Issue numberPART 2
    DOIs
    Publication statusPublished (in print/issue) - 2010
    Event5th International Conference on Hybrid Artificial Intelligence Systems, HAIS 2010 - San Sebastian, Spain
    Duration: 23 Jun 201025 Jun 2010

    Keywords

    • α-lock resolution method
    • α-resolution principle
    • α-satisfiability
    • lattice-valued logic

    Fingerprint

    Dive into the research topics of 'α-satisfiability and α-lock resolution for a lattice-valued logic LP(X)'. Together they form a unique fingerprint.

    Cite this