Abstract of Paper

Derivability in Locally Quantified Modal Logics via Translation in Set Theory
by Angelo Montanari, Alberto Policriti, Matteo Slanina


Two among the most active research areas in automated deduction in modal
logic are the employment of translation methods to reduce its derivability
problem to that of classical logic and the extension of existing automated
reasoning techniques, developed initially for the propositional case, to
first-order modal logics. This paper addresses both issues by extending the
translation method for propositional modal logics known as
\emph{$\Box$-as-Pow} (read ``box-as-powerset'') to a widely used class of
first-order modal logics, namely, the class of \emph{locally quantified}
modal logics. To do this, we prove a more general result that allows us to
separate (classical) first-order from modal (propositional) reasoning. Our
translation can be seen as an example application of this result, in both
definition and proof of adequateness.