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
    CountryTaiwan, Republic of China
    CityTaipei
    Period24/11/1527/11/15

    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