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 propose applies to any normal complete finitely-axiomatizable polymodal logic, regardless if it is first-order complete. 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.
A set-theoretic translation method for (poly)modal logics
D'AGOSTINO, Giovanna;MONTANARI, Angelo;POLICRITI, Alberto
1995-01-01
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 propose applies to any normal complete finitely-axiomatizable polymodal logic, regardless if it is first-order complete. 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
