Sciweavers

Share
ENTCS
2010

A Tableau Method for Checking Rule Admissibility in S4

11 years 5 months ago
A Tableau Method for Checking Rule Admissibility in S4
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 firstorder 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.
Sergey Babenyshev, Vladimir V. Rybakov, Renate A.
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2010
Where ENTCS
Authors Sergey Babenyshev, Vladimir V. Rybakov, Renate A. Schmidt, Dmitry Tishkovsky
Comments (0)
books