Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic

Yang Xu, Jun Liu, Xingxing He, Xiaomei Zhong, Shuwei Chen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    4 Citations (Scopus)

    Abstract

    The present paper focuses on a resolution-based automated reasoning theory in a lattice-valued logic system with truth-values defined in a lattice-valued algebraic structure - lattice implication algebras (LIA) in order to handle automated deduction under an uncertain environment. Particularly, as a continuation and extension of the established work on binary resolution at a certain truth-value level a (called a-resolution), a non-clausal multi-ary a-generalized resolution principle and deduction are introduced in this paper for a lattice-valued first-order logic LF(X) based on LIA, which is essentially non-clausal generalized resolution avoiding the reduction to normal clausal form. Non-clausal multi-ary a-generalized resolution deduction in LF(X) is then proved to be sound and complete. The present work is expected to provide a theoretical foundation of more efficient resolution based automated reasoning in lattice-valued logic.

    Original languageEnglish
    Title of host publicationProceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015
    PublisherInstitute of Electrical and Electronics Engineers Inc.
    Pages1-7
    Number of pages7
    ISBN (Electronic)9781467393225
    DOIs
    Publication statusPublished - 13 Jan 2016
    Event10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015 - Taipei, Taiwan, Republic of China
    Duration: 24 Nov 201527 Nov 2015

    Publication series

    NameProceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015

    Conference

    Conference10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015
    Country/TerritoryTaiwan, Republic of China
    CityTaipei
    Period24/11/1527/11/15

    Bibliographical note

    Publisher Copyright:
    © 2015 IEEE.

    Keywords

    • Automated reasoning
    • Lattice implication algebra
    • Latticevalued logic
    • Non-clausal multi-ary - generalized resolution
    • Resolution principle

    Fingerprint

    Dive into the research topics of 'Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic'. Together they form a unique fingerprint.

    Cite this