Axiomatic and Tableau-Based Reasoning for Kt(H, R)

Renate Schmidt, John G Stell, David E Rydeheard

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


    We introduce a tense logic, called Kt (H, R), arising from logics for spatial reasoning. Kt (H,R) is a multi-modal logic with two modalities and their converses defined with respect to a pre-order and a relation stable over this pre-order. We show Kt (H, R) is decidable, it has the effective finite model property and reasoning in Kt (H, R) is PSPACE-complete. Two complete Hilbert-style axiomatisations are given. The main focus of the paper is tableau-based reasoning.
    Original languageEnglish
    Title of host publicationAdvances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic," held in Groningen, The Netherlands, August 5-8, 2014
    Number of pages20
    Publication statusPublished - 2014
    EventAIML 10 - Groningen, The Netherlands
    Duration: 5 Aug 20148 Aug 2014


    ConferenceAIML 10
    CityGroningen, The Netherlands
    Internet address


    Dive into the research topics of 'Axiomatic and Tableau-Based Reasoning for Kt(H, R)'. Together they form a unique fingerprint.

    Cite this