A bi-intuitionistic modal logic: foundations and automation (Q299186): Difference between revisions

From MaRDI portal
RedirectionBot (talk | contribs)
Changed an Item
Changed an Item
Property / describes a project that uses
 
Property / describes a project that uses: MetTeL / rank
 
Normal rank

Revision as of 02:08, 28 February 2024

scientific article
Language Label Description Also known as
English
A bi-intuitionistic modal logic: foundations and automation
scientific article

    Statements

    A bi-intuitionistic modal logic: foundations and automation (English)
    0 references
    0 references
    0 references
    0 references
    22 June 2016
    0 references
    In the paper, a bi-intuitionistic logic BISKT with modal tense operators is constructed. This logic finds its foundations in a general algebraic framework of pre-orders and relations on downward-closed sets as well as on graphs. Then, BISKT can be defined as a bi-intuitionistic stable tense logic with a semantics in which formulas are interpreted as downward-closed sets, including subgraphs as a special case. The language of BISKT includes two adjoint pairs of modal tense operators: \(\square\), \(\blacklozenge\), \(\lozenge\), \(\blacksquare\). These operators obtain their interpretation on subgraphs by taking the nodes to be time points, the edges to be open intervals, and \(R\) to relate each open interval to all instants that either end the interval or end some later interval. As the authors explain, the times when, e.g., \(\lozenge p\) holds are then the open intervals for which \(p\) holds at some later instant, together with both endpoints of those intervals, and the times when \(\blacksquare q\) holds are all the closed intervals where \(q\) holds at all times and has always held. Remarkably, an alternative semantics for BISKT can be obtained by its embedding into the traditional propositional tense logic \(Kt(H,R)\) defined over two accessibility relations \(H\) and \(R\) and their converse relations. Since it is well-known that \(Kt(H,R)\) is decidable and has the effective finite model property, it follows that BISKT has the effective finite model property and is decidable as well. Moreover, it can be shown that satisfiability in BISKT is PSPACE-complete. The paper also presents a terminating labeled tableau calculus for BISKT, which is shown to be sound and complete.
    0 references
    temporal logic
    0 references
    bi-intuitionistic logic
    0 references
    tableau system
    0 references
    decidability
    0 references
    correspondence theorem
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references