A tableau-like proof procedure for normal modal logics (Q1329745)

This is an extension to modal logic of the following proof search procedure for classical propositional logic: Expand the goal formula \(G\) into conjunctive normal form and apply the resolution method to the resulting set of clauses. Since these rules of expansion are dual to the standard Gentzen-type rules, the author uses the term ``dual clauses''. The Kripke-style formulation used here derives objects \((k_ 1 F_ 1,\dots, k_ n F_ n)\) with the interpretation: Formula \(F_ 1\) is true in the world \(k_ 1,\dots, F_ n\) is true in \(k_ n\). A modal rule for \(\square A\) is the same as a Kripke rule, but the rule for \(\diamondsuit\) is dual to a Kripke rule: Instantiation \(k'A\) of a formula \(k\diamondsuit A\) for a world \(k'\) accessible from \(k\), generates a new branch of the proof search tree. Another source of branching is the rule for \(V\), while the rule for \((A \& B)\) adds both components \(A\), \(B\) to the same branch. Each branch \(\mathcal B\) (at each stage of construction) of the proof search tree generates a clause \(C_{\mathcal B}\) consisting of (possibly negated) new propositional variables \(p_ k\) obtained from formulas \(kp\), \(k\neg p\) present in \(\mathcal B\). The tree is a proof if the set of clauses corresponding to all branches is inconsistent. The latter property can be checked by propositional resolution. Extensions to predicate logics with constant and expanding domains are sketched. Implementation of the method is mentioned, but no test results are presented. It would be interesting to compare this construction with Beth models and to describe a modification for intuitionistic logic which does not require Gödel-Tarski translation.