Developing modal tableaux and resolution methods via first-order resolution

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

    Abstract

    This paper explores the development of calculi using different proof methods for propositional dynamic modal logics. Dynamic modal logics are PDL-like extended modal logics which are closely related to description logics. We show how tableau systems, modal resolution systems and Rasiowa-Sikorski systems, which are dual tableau systems, can be developed and studied by using standard principles and methods of first-order theorem proving. We translate modal logic reasoning problems to first-order clausal form and then use a suitable refinement of resolution to construct and mimic derivations using the desired proof method. The inference rules of the calculus can then be read off from the clausal form used. © 2006, Renate A. Schmidt.
    Original languageEnglish
    Title of host publicationAdvances in Modal Logic 2006|Adv. Modal Logic
    Pages1-26
    Number of pages25
    Volume6
    Publication statusPublished - 2006
    Event6th Conference on Advances in Modal Logic, AiML-2006 - Noosa, QLD
    Duration: 1 Jul 2006 → …

    Conference

    Conference6th Conference on Advances in Modal Logic, AiML-2006
    CityNoosa, QLD
    Period1/07/06 → …

    Keywords

    • Decidability
    • Deduction
    • Dual resolution
    • Dual tableaux
    • Modal logic
    • Modal resolution
    • Resolution
    • Tableaux

    Fingerprint

    Dive into the research topics of 'Developing modal tableaux and resolution methods via first-order resolution'. Together they form a unique fingerprint.

    Cite this