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

Title of this publication is not available (Why is that?)

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

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)

Cited In (7)

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

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)