A novel generalization of resolution principle for automated deduction

Yang Xu, Jun Liu, Shuwei Chen, Xiaomei Zhong

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

    5 Citations (Scopus)

    Abstract

    Resolution principle proposed originally by Robinson in 1965 has dominated automated deduction for over three decades while the current most successful automated deduction systems are based on resolution. In this paper, we consider a generalization of the standard resolution principle and their variation since then, it is proposed as a multi-ary, dynamic, contradiction separation based inference rule for automated deduction, where the existing resolution rule and its variations are its special cases. The key concepts and some conclusions are briefly outlined in this short paper.

    Original languageEnglish
    Title of host publicationUncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016
    EditorsJie Lu, Ludovic Koehl, Etienne E. Kerre, Luis Martinez, Xianyi Zeng
    PublisherWorld Scientific Publishing Co. Pte Ltd
    Pages483-488
    Number of pages6
    ISBN (Electronic)9789813146969
    DOIs
    Publication statusPublished - 2016
    EventUncertainty Modelling in Knowledge Engineering and Decision Making - 12th International Fuzzy Logic and Intelligent Technologies in Nuclear Science Conference, FLINS 2016 - Roubaix, France
    Duration: 24 Aug 201626 Aug 2016

    Publication series

    NameUncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016

    Conference

    ConferenceUncertainty Modelling in Knowledge Engineering and Decision Making - 12th International Fuzzy Logic and Intelligent Technologies in Nuclear Science Conference, FLINS 2016
    CountryFrance
    CityRoubaix
    Period24/08/1626/08/16

    Keywords

    • Automated deduction
    • Contradiction separation
    • Resolution

    Fingerprint

    Dive into the research topics of 'A novel generalization of resolution principle for automated deduction'. Together they form a unique fingerprint.

    Cite this