Tableaux for Logics of Subinterval Structures over Dense Orderings

Davide Bresolin, Valentin Goranko, Angelo Montanari, Pietro Sala

    Research output: Contribution to journalConference articleResearchpeer-review

    Abstract

    In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec.
    Original languageEnglish
    JournalJournal of Logic and Computation
    Volume20
    Issue number1
    Pages (from-to)133-166
    ISSN0955-792X
    DOIs
    Publication statusPublished - 2010
    EventInternational Conference on Automated Reasoning with Analytic Tableaux and Related Methods - Aix en Provence, FRANCE,
    Duration: 1 Jan 2007 → …
    Conference number: 16th

    Conference

    ConferenceInternational Conference on Automated Reasoning with Analytic Tableaux and Related Methods
    Number16th
    CityAix en Provence, FRANCE,
    Period01/01/2007 → …

    Fingerprint Dive into the research topics of 'Tableaux for Logics of Subinterval Structures over Dense Orderings'. Together they form a unique fingerprint.

    Cite this