

Logics Modulo Theories, LMT, is a logical framework specially designed to support the work of multi-agent systems. It is a system that allows local logics to communicate through a global system which has its own logic. (The method has similarities with, but goes beyond, SMT, Satisfiability Modulo Theories.) In two earlier papers we considered a variety of logics used to represent ontologies (e.g. first order logic, description logic) as the local logics and at the global level we used a propositional logic. However, at that time, we only gently hinted how this applies to multi-agent systems and we lacked quantification capabilities in the upper logic. In this paper we present full blown support for multi-agent system, the use of the modal logic S5 at the global level. The following are the theses of this paper : a) when used for combining logics, in comparison to other methods, LMT produces a more elegant and simpler logical system which is appropriate for multi-agent work, b) the ideal properties of its component logics, namely – soundness and completeness transfer to the resulting logic, c) the proofs for these are very straightforward because LMT uses well-established technology.