A tableau method for checking rule admissibility in S4

DOI10.1016/J.ENTCS.2010.04.003MaRDI QIDQ3185759zbMATH OpenOpenAlexFDO

Authors Sergey Babenyshev, Renate A. Schmidt, Dmitry Tishkovsky, Vladimir 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

\textsf{S4}admissible rulemodal logictableau calculustableau synthesis framework

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4204318
• scientific article; zbMATH DE number 3959387
• scientific article; zbMATH DE number 2079050
• Admissible rules for logics containing S4.3
• Proof theory for admissible rules

Cites work

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

Cited in

(11)

• Extending unification in \(\mathcal{EL}\) to disunification: the case of dismatching and local disunification
• \textsc{MetTeL}: a tableau prover with logic-independent inference engine
• Simulation and synthesis of deduction calculi
• Machine-checked proof-theory for propositional modal logics
• Unification in epistemic logics
• KD is nullary
• Multi-Agents’ Temporal Logic using Operations of Static Agents’ Knowledge
• Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition
• Best unifiers in transitive modal logics
• Unification in linear temporal logic LTL
• Temporal logic with accessibility temporal relations generated by time states themselves

This page was built for publication: A tableau method for checking rule admissibility in S4

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3185759)