zbMATH — the first resource for mathematics

Efficient strategies for automated reasoning in modal logics. (English) Zbl 0988.03508
MacNish, Craig (ed.) et al., Logics in artificial intelligence. European Workshop JELIA ’94, York, GB, September 5-8, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 838, 182-197 (1994).
Summary: In automated deduction for nonclassical logics and especially for modal logics, efficient (and not only complete) strategies are needed. Ordering strategies are presented for Fitting’s tableaux calculi. Besides orderings of tableaux rules, different variants for backtracking are used. The strategies apply to most usual propositional modal logics: K, T, K4, S4, D, D4, C, CT, C4, CS4, CD, CD4, G. More precisely, they apply to logics for which there exists a tableaux calculus such that the number of sets of formulas introduced in a tree is finite – the analytic tableaux systems satisfy this requirement. The strategies are proved to be complete for most of these logics. The results are presented for S4. The strategies have been implemented and extensively experimented in the tableaux theorem prover running on our Inference Laboratory ATINF. Experiments have shown the efficiency of some of the proposed strategies.
For the entire collection see [Zbl 0849.00036].
03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)