scientific article; zbMATH DE number 1735878

zbMATH Open0993.03017MaRDI QIDQ4329239FDOQ4329239

Authors Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt

Publication date 29 April 2002

zbMATH Keywords

resolution decision proceduretransitive propositional modal logics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1215470
• A loop-free decision procedure for modal propositional logics K4, S4 and S5
• Resolution-based methods for modal logics
• Publication:4207883
• Modal resolution in clausal form

Cited in

(8)

• Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
• First-order resolution methods for modal logics
• Automated theorem proving by resolution in non-classical logics
• Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
• Modal Satisfiability via SMT Solving
• Harald Ganzinger's legacy: contributions to logics and programming
• A loop-free decision procedure for modal propositional logics K4, S4 and S5
• Improved decision procedures for the modal logics K, T and S4

This page was built for publication:

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