Modal Tableaux with Propagation Rules and Structural Rules

Castilho, Marcos and Farinas del Cerro, Luis and Gasquet, Olivier and Herzig, Andreas

Abstract:

In this paper we generalize the existing tableau methods for modal logics. First of all, while usual modal tableaux are based on trees, our basic structures are rooted directed acyclic graphs (RDAG). This allows natural tableau rules for some modal logics that are difficult to capture in the usual way (such as those having an accessibility relation that is dense or confluent). Second, tableau rules rewrite patterns, which are (schemas of) parts of a RDAG. A particular case of these rules are the single-step rules recently proposed by Massacci. This allows in particular tableau rule presentations for K5, KD5, K45, KD45, and S5 that respect the subformula property. Third, we divide modal tableau rules into propagation rules and structural rules. Structural rules construct new edges and nodes (without adding formulas to nodes), while propagation rules add formulas to nodes. This distinction allows to prove completeness in a modular way.

PDF PostScript PostScript, gzipped

Bibtex-entry:


@Article{CaFaGaHe-FI97,
  author =   "Castilho, M. and Fari{\~{n}}as del Cerro, L. and Gasquet, O. and Herzig, A." ,
  title =    "Modal Tableaux with Propagation Rules and Structural Rules",
  journal =      "Fundamenta Informaticae",
  year =     "1997",
  volume =   "32",
  number =   "3/4",
  pages =    "",
}

https://www.irit.fr/~Olivier.Gasquet