Automated theorem proving by resolution in non-classical logics

We present several classes of non-classical logics (many of which are practically relevant in knowledge representation) which can be translated into tractable and relatively simple fragments of classical logic. In this context, refinements of resolution can be often used successfully for automated theorem proving, and in many cases yield optimal decision procedures