A Tableau Method for Checking Rule Admissibility in S4

Babenyshev, S. and Rybakov, V. and Schmidt, R. A. and Tishkovsky, D. (2010)

Electronic Notes in Theoretical Computer Science 262 17-32. BiBTeX, PDF, DOI Link.

Rules that are admissible can be used in any derivations in any axiomatic system of a logic. In this paper we introduce a method for checking the admissibility of rules in the modal logic S4. Our method is based on a standard semantic ground tableau approach. In particular, we reduce rule admissibility in S4 to satisfiability of a formula in a logic that extends S4. The extended logic is characterised by a class of models that satisfy a variant of the co-cover property. The class of models can be formalised by a well-defined first-order specification. Using a recently introduced framework for synthesising tableau decision procedures this can be turned into a sound, complete and terminating tableau calculus for the extended logic, and gives a tableau-based method for determining the admissibility of rules.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 15 Jun 10
Copyright © 2010 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk