A tableau-like proof procedure for normal modal logics

DOI10.1016/0304-3975(94)90085-XMaRDI QIDQ1329745zbMATH OpenFDO

Authors Zoran Ognjanović

Publication date 29 January 1995

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(94)90085-X

zbMATH Keywords

dual clauses proof search procedure proof search tree

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

Review text

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.

Recommendations

Cites work

Cited in

(5)

Describes a project that uses

Uses Software

This page was built for publication: A tableau-like proof procedure for normal modal logics

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