Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Terminating Hybrid Tableaus for Ordered Models

Yuki Nishimura

TL;DR

The paper tackles the decision problem for hybrid logics with nominals over ordered model classes by introducing terminating tableau calculi TAB_I4, TAB_I4D, and TAB_PO for SPO, USPO, and PO models, respectively. Central to the approach is bulldozing, a transformation that reshapes countermodels into irreflexive or ordered forms, enabling finite termination even when infinite countermodels might exist. The authors prove termination and completeness for all three calculi, providing a decidable framework for hybrid logics on ordered structures. This work advances proof theory for hybrid logics by delivering concrete, terminating procedures that handle non-finite frame properties via finite completions and model reductions, with potential extensions to total orders and broader axiom sets.

Abstract

Hybrid logic extends modal logic with special propositions called nominals, each of which is true at only one state in a model. This enables us to describe some properties of binary relations, such as irreflexivity and anti-symmetry, which are essential to treat partial orders. We present terminating tableau calculi complete with respect to models whose accessibility relations are strictly partially ordered, unbounded strictly partially ordered, and partially ordered.

Terminating Hybrid Tableaus for Ordered Models

TL;DR

The paper tackles the decision problem for hybrid logics with nominals over ordered model classes by introducing terminating tableau calculi TAB_I4, TAB_I4D, and TAB_PO for SPO, USPO, and PO models, respectively. Central to the approach is bulldozing, a transformation that reshapes countermodels into irreflexive or ordered forms, enabling finite termination even when infinite countermodels might exist. The authors prove termination and completeness for all three calculi, providing a decidable framework for hybrid logics on ordered structures. This work advances proof theory for hybrid logics by delivering concrete, terminating procedures that handle non-finite frame properties via finite completions and model reductions, with potential extensions to total orders and broader axiom sets.

Abstract

Hybrid logic extends modal logic with special propositions called nominals, each of which is true at only one state in a model. This enables us to describe some properties of binary relations, such as irreflexivity and anti-symmetry, which are essential to treat partial orders. We present terminating tableau calculi complete with respect to models whose accessibility relations are strictly partially ordered, unbounded strictly partially ordered, and partially ordered.

Paper Structure

This paper contains 16 sections, 29 theorems, 28 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Background and Results
  3. Related Works
  4. Organization of the Paper
  5. Preliminaries
  6. Kripke Semantics for Hybrid Logic
  7. Basic Tableau Calculus
  8. Tableau Calculus for Strict Partial Order
  9. Definition
  10. Termination Property
  11. Completeness
  12. Tableau Calculus for Unbounded Strict Partial Order
  13. Tableau Calculus for Partial Order
  14. Termination Property
  15. Completeness
  16. ...and 1 more sections

Key Result

Theorem 2.10

The tableau calculus $\mathbf{TAB}$ has the termination property. That is, for every tableau in $\mathbf{TAB}$ is finite.

Figures (9)

  • Figure 1: The rules of $\mathbf{TAB}$
  • Figure 2: A closed tableau of $\mathbf{TAB}$. Formulas with ${}^*$ are accessibility formulas.
  • Figure 3: Additional rules
  • Figure 4: Non-terminating tableau of $\mathbf{TAB}$ with $[\mathit{Trs}]$. Formulas with ${}^*$ are accessibility formulas.
  • Figure 5: Another example of tableau terminated due to $(\mathcal{D})$. Formulas with ${}^*$ are accessibility formulas.
  • ...and 4 more figures

Theorems & Definitions (77)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Definition 2.8
  • Definition 2.9
  • Theorem 2.10
  • ...and 67 more