A Set-Theoretic Translation Method for Polymodal Logics
Giovanna D'Agostino, Angelo Montanari, Alberto Policriti

Abstract:
The paper presents a set­theoretic translation method for polymodal logics 
that reduces the derivability problem of a large class of propositional 
polymodal logics to the derivability problem of a very weak first­order set
theory \Omega. Unlike most existing translation methods, the one we proposed 
applies to any normal complete finitely­axiomatizable polymodal logic, 
regardless if it is first­order complete or if an explicit semantics is 
available for it. Moreover, the finite axiomatizability of \Omega makes it 
possible to implement mechanical proof search procedures via the deduction 
theorem or more specialized and efficient techniques.
In the last part of the paper, we briefly discuss the application of set T­
resolution to support automated derivability in (a suitable extension of) 
\Omega.