A Tableau Method for Checking Rule Admissibility in S4

DOI10.1016/j.entcs.2010.04.003zbMath1345.03033OpenAlexW2114356493MaRDI QIDQ3185759

Sergey Babenyshev, Dmitry Tishkovsky, Renate A. Schmidt, Vladimir Vladimirovich Rybakov

Publication date: 5 August 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2010.04.003

zbMATH Keywords

modal logictableau calculusadmissible rule\textsf{S4}tableau synthesis framework

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Related Items (9)

Simulation and Synthesis of Deduction Calculi ⋮ Multi-Agents’ Temporal Logic using Operations of Static Agents’ Knowledge ⋮ Unification in epistemic logics ⋮ KD is nullary ⋮ Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification ⋮ Best unifiers in transitive modal logics ⋮ $\textsc{Met\hspace{-.5pt}TeL}$ : A Tableau Prover with Logic-Independent Inference Engine ⋮ Unification in linear temporal logic LTL ⋮ Temporal logic with accessibility temporal relations generated by time states themselves

Cites Work

• Unnamed Item
• Unnamed Item
• Complexity of admissible rules
• A criterion for admissibility of rules in the modal system S4 and intuitionistic logic
• Derivability of admissible rules
• Admissibility of logical inference rules
• The decidability of admissibility problems for modal logics S4.2 and S4.2Grz and superintuitionistic logic KC
• Best solving modal equations
• On the admissible rules of intuitionistic propositional logic
• A Resolution/Tableaux Algorithm for Projective Approximations in IPC
• Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
• A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
• Rules of inference with parameters for intuitionistic logic
• One hundred and two problems in mathematical logic
• Unification in intuitionistic logic
• Admissible and derivable rules in intuitionistic logic
• On Finite Model Property for Admissible Rules
• Undecidability of the unification and admissibility problems for modal and description logics
• Filtering unification and most general unifiers in modal logic
• Admissible Rules of Modal Logics
• Automated Synthesis of Tableau Calculi

This page was built for publication: A Tableau Method for Checking Rule Admissibility in S4