Output details

A Tableau Method for Checking Rule Admissibility in S4

<11> A key question in applications requiring reasoning is which inference rules may be used and how; rule admissibility deals with the first part of the question. While in general rule admissibility is difficult (undecidable), the paper makes a significant contribution by presenting a practical tableau decision procedure for the problem of determining the admissibility of inference rules for modal logic S4. This is obtained from a mathematically rigorous formalisation of the problem using our tableau synthesis framework (slightly extended). As an important side-effect the work demonstrates the generality and usefulness of tableau synthesis.