A tableau method for checking rule admissibility in S4. (English) Zbl 1345.03033
Bolander, Thomas (ed.) et al., Proceedings of the 6th workshop on methods for modalities (M4M-6 2009), Copenhagen, Denmark, November 12–14, 2009. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 262, 17-32 (2010).
Summary: 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.
For the entire collection see [Zbl 1281.03003].
For the entire collection see [Zbl 1281.03003].
MSC:
| 03B45 | Modal logic (including the logic of norms) |
References:
| [1] | Babenyshev, S., The decidability of admissibility problems for modal logics S4.2 and S4.2Grz and superintuitionistic logic KC, Algebra Logic, 31, 4, 205-216 (1992) · Zbl 0795.03017 |
| [2] | Friedman, H., One hundred and two problems in mathematical logic, J. Symb. Log., 40, 3, 113-130 (1975) · Zbl 0318.02002 |
| [3] | Ghilardi, S., Unification in intuitionistic logic, J. Symb. Log., 64, 2, 859-880 (1999) · Zbl 0930.03009 |
| [4] | Ghilardi, S., Best solving modal equations, Ann. Pure Appl. Logic, 102, 3, 183-198 (2000) · Zbl 0949.03010 |
| [5] | Ghilardi, S., A resolution/tableaux algorithm for projective approximations in IPC, Log. J. IGPL, 10, 3, 229-243 (2002) · Zbl 1005.03504 |
| [6] | Ghilardi, S.; Sacchetti, L., Filtering unification and most general unifiers in modal logic, J. Symb. Log., 69, 3, 879-906 (2004) · Zbl 1069.03011 |
| [7] | Harrop, R., Concerning formulas of the types \(a \to b \vee c, a \to \exists x b(x)\) in intuitionistic formal system, J. Symb. Log., 25, 27-32 (1960) · Zbl 0098.24201 |
| [8] | Iemhoff, R., On the admissible rules of intuitionistic propositional logic, J. Symb. Log., 66, 1, 281-294 (2001) · Zbl 0986.03013 |
| [9] | Jeřábek, E., Admissible rules of modal logics, J. Log. Comput., 15, 4, 411-431 (2005) · Zbl 1077.03011 |
| [10] | Jeřábek, E., Complexity of admissible rules, Arch. Math. Logic, 46, 2, 73-92 (2007) · Zbl 1115.03010 |
| [11] | Kiyatkin, V. R.; Rybakov, V. V.; Oner, T., On finite model property for admissible rules, Mathematical Logic Quarterly, 45, 505-520 (1999) · Zbl 0938.03033 |
| [12] | Lorenzen, P., Einführung in die operative Logik und Mathematik (1955), Springer · Zbl 0066.24802 |
| [13] | Mints, G., Derivability of admissible rules, Journal of Soviet Mathematics, 6, 4, 417-421 (1976) · Zbl 0375.02014 |
| [14] | Roziere, P., Admissible and derivable rules, Mathematical Structures in Computer Science, 3, 129-136 (1993) · Zbl 0797.03001 |
| [15] | Rybakov, V. V., A criterion for admissibility of rules in modal system S4 and the intuitionistic logic, Algebra Logic, 23, 5, 369-384 (1984) · Zbl 0598.03013 |
| [16] | Rybakov, V. V., Semantic admissibility criteria for deduction rules in S4 and Int, Mat. Zametki, 50, 1, 84-91 (1991) · Zbl 0729.03013 |
| [17] | Rybakov, V. V., Rules of inference with parameters for intuitionistic logic, J. Symb. Log., 57, 3, 912-923 (1992) · Zbl 0788.03007 |
| [18] | Rybakov, V. V., Admissibility of logical inference rules, Studies in Logic and the Foundations of Mathematics, vol. 136 (1997), Elsevier · Zbl 0872.03002 |
| [19] | Rybakov, V. V., Logics with universal modality and admissible consecutions, J. Appl. Non-Classical Log., 17, 3, 381-394 (2007) |
| [20] | Schmidt, R. A.; Tishkovsky, D., Using tableau to decide expressive description logics with role negation, (ISWC07. ISWC07, Lect. Notes Comput. Sci., vol. 4825 (2007), Springer), 438-451 |
| [21] | Schmidt, R. A.; Tishkovsky, D., A general tableau method for deciding description logics, modal logics and related first-order fragments, (IJCAR08. IJCAR08, Lect. Notes Comput. Sci., vol. 5195 (2008), Springer), 194-209 · Zbl 1165.03319 |
| [22] | Schmidt, R. A.; Tishkovsky, D., Automated synthesis of tableau calculi, (TABLEAUX09. TABLEAUX09, Lect. Notes Artif. Intell., vol. 5607 (2009), Springer), 310-324 · Zbl 1218.03011 |
| [23] | Wolter, F.; Zakharyaschev, M., Undecidability of the unification and admissibility problems for modal and description logics, ACM Transdactions on Computational Logic, 9, 4, 1-20 (2008) · Zbl 1367.03026 |
| [24] | D. Zucchelli. Studio e realizzazione di algoritmi per l’unificazione nelle logiche modali. Laurea specialistica in informatica (Masters Thesis), Università degli Studi di Milano, 2004. In Italian. Supervisor: Silvio Ghilardi; D. Zucchelli. Studio e realizzazione di algoritmi per l’unificazione nelle logiche modali. Laurea specialistica in informatica (Masters Thesis), Università degli Studi di Milano, 2004. In Italian. Supervisor: Silvio Ghilardi |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
