Abstract

In this work, the problem of performing abduction in modal logics is addressed, along the lines of [3], where a proof theoretical abduction method for full first order classical logic is defined, based on tableaux and Gentzen-type systems. This work applies the same methodology to face modal abduction. The non-classical context enforces the value of analytical proof systems as tools to face the meta-logical and proof-theoretical questions involved in abductive reasoning.The similarities and differences between quantifiers and modal operators are investigated and proof theoretical abduction methods for the modal systems K, D, T and S4 are defined, that are sound and complete. The construction of the abductive explanations is in strict relation with the expansion rules for the modal logics, in a modular manner that makes local modifications possible. The method given in this paper is general, in the sense that it can be adapted to any propositional modal logic for which analytic tableaux are provided. Moreover, the way towards an extension to first order modal logic is straightforward