A Resolution-Based Calculus for Preferential Logics

Cláudia Nalon*, Dirk Pattinson

*Corresponding author for this work

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

    3 Citations (Scopus)

    Abstract

    The vast majority of modal theorem provers implement modal tableau, or backwards proof search in (cut-free) sequent calculi. The design of suitable calculi is highly non-trivial, and employs nested sequents, labelled sequents and/or specifically designated transitional formulae. Theorem provers for first-order logic, on the other hand, are by and large based on resolution. In this paper, we present a resolution system for preference-based modal logics, specifically Burgess’ system. Our main technical results are soundness and completeness. Conceptually, we argue that resolution-based systems are not more difficult to design than cut-free sequent calculi but their purely syntactic nature makes them much better suited for implementation in automated reasoning systems.

    Original languageEnglish
    Title of host publicationAutomated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
    EditorsRoberto Sebastiani, Didier Galmiche, Stephan Schulz
    PublisherSpringer Verlag
    Pages498-515
    Number of pages18
    ISBN (Print)9783319942049
    DOIs
    Publication statusPublished - 2018
    Event9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
    Duration: 14 Jul 201817 Jul 2018

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume10900 LNAI
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
    Country/TerritoryUnited Kingdom
    CityOxford
    Period14/07/1817/07/18

    Fingerprint

    Dive into the research topics of 'A Resolution-Based Calculus for Preferential Logics'. Together they form a unique fingerprint.

    Cite this