The recursive resolution method for modal logic

DOI10.1007/BF03037397MaRDI QIDQ1104915zbMATH OpenFDO

Authors Man-chung Chan

Publication date 1987

Published in New Generation Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF03037397

zbMATH Keywords

modal logicmodal normal formmodal resolvabilityRecursive ResolutionS4Skolem operatorstransformation process for modal clauses

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04) Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

Review text

The author suggests a syntactic proof procedure for the modal logic system S4 avoiding explicit construction of possible worlds or reduction of modalities by quantified variables. The basic approach mirrors that of Robinson's resolution for predicate calculus. The originality rises from the introduction of a transformation process for modal clauses which ``Skolemizes the possibility operator. It results in obtaining modal clauses in special normal form (m-clause), which can be further processed by the proof procedure called Recursive Resolution (RR). Modal resolution criterion (MRC) is one of the milestones of this procedure. MRC is specified in form of an algorithm (its implementation in Franz LISP is listed in the Appendix), its basic property is stated by the following Theorem 1: A pair of complementary \(m\)-literals is inconsistent iff they satisfy the MRC. Modal resolvability of two \(m\)-clauses is defined through 5 special recursive rules, denoted by SRR, the application of which is proved to be sound. The author conjectures that the SRR rules form a complete decision procedure for a notationally restricted propositional S4.

Recommendations

• scientific article; zbMATH DE number 4128785
• scientific article; zbMATH DE number 1880278
• Modal resolution in clausal form
• Linear strategy for propositional modal resolution
• scientific article; zbMATH DE number 4055570

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• scientific article; zbMATH DE number 4014675 (Why is no real title available?)
• scientific article; zbMATH DE number 3114382 (Why is no real title available?)
• scientific article; zbMATH DE number 3325547 (Why is no real title available?)
• Methods for Automated Theorem Proving in Nonclassical Logics
• Theorem-Proving on the Computer

Cited in

(13)

• MOLOG: A system that extends PROLOG with modal logic
• Linear strategy for propositional modal resolution
• A resolution framework for finitely-valued first-order logics
• A tableau-like proof procedure for normal modal logics
• scientific article; zbMATH DE number 4018413 (Why is no real title available?)
• scientific article; zbMATH DE number 5295699 (Why is no real title available?)
• scientific article; zbMATH DE number 4128785 (Why is no real title available?)
• Resolution-based methods for modal logics
• scientific article; zbMATH DE number 1880278 (Why is no real title available?)
• Modal Resolution
• Resolution calculi for non-normal modal logics
• A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics
• Non-iterative modal resolution calculi

This page was built for publication: The recursive resolution method for modal logic

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