Translating a Modal Language with Embedded Implications into Horn Clause Logic

In this paper we present a method for translating Horn clauses extended with modalities and embedded implication (which provide reasoning capabilities in a multiagent situation and hypothetical reasoning) into Horn clauses, therefore suitable for SLD resolution. The translation takes two steps: the first one eliminates embedded implications by introducing new modalities; the second eliminates modalities by adding an argument which represents the worlds of the Kripke semantics to all predicates.