Subsumption in modal logic

"Subsumption has long been known as a technique to detect redundant clauses in the search space of automated deduction systems for classical first order logic. In recent years several automated deduction methods for non-classical modal logics have been developed. This thesis explores, how subsumption can be made to work in the context of these modal logic deduction methods.Many modern modal logic deduction methods follow an indirect approach. They translate the modal sentences into some other target language, and then determine whether there exists a proof in that language, rather than doing deduction in the modal language itself. Consequently, subsumption then needs to focus on the target language, in which the actual proof is done.World Path Logic (WPL) is introduced as a possible target language. Deduction in WPL works very much like in ordinary logic, the only significant difference is the need for a special purpose unification, which unifies world paths under an equational theory (E-unification). Relating WPL to a well understood first order logic of restricted quantification, the properties of WPL, that make deduction work, are examined. The obtained theoretical results are the basis for the following treatment of subsumption in WPL.Subsumption is analyzed treating a clause as a scheme standing for the set of its ground instances. Although the notion of ground instances in WPL is different from ordinary logic, it turns out that -- just like in ordinary logic -- a clause Cl subsumes another clause C2, if there exists a substitution θ such that C1θ ⊆ C2. Once the special purpose unification has been implemented into a theorem prover to allow for deduction in WPL, existing subsumption tests then work without any further changes.