zbMATH — the first resource for mathematics

Mechanised reasoning and model generation for extended modal logics. (English) Zbl 1203.03020
de Swart, Harrie (ed.) et al., Theory and applications of relational structures as knowledge instruments. COST Action 274, TARSKI. Revised papers. Berlin: Springer (ISBN 3-540-20780-5/pbk). Lect. Notes Comput. Sci. 2929, 38-67 (2003).
Summary: The approach presented in this overview paper exploits that modal logics can be seen to be fragments of first-order logic and deductive methods can be developed and studied within the framework of first-order resolution. We focus on a class of extended modal logics very similar in spirit to propositional dynamic logic and closely related to description logics. We review and discuss the development of decision procedures for decidable extended modal logics and look at methods for automatically generating models.
For the entire collection see [Zbl 1029.00017].

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