Automated theorem proving by resolution in non-classical logics (Q2385426)

The main goal of the paper is to find uniform principles, applicable to large classes, which lead to simple and reusable implementations. The author presents several situations in which nonclassical logics can be translated into tractable and simple fragments of classical logic and resolution can be used successfully for automated theorem proving. The main advantage of such an approach is that it allows one to use existing automated theorem provers. She shows in this paper that in many interesting situations translations into classical logic allows one to obtain decision procedures of optimal complexity. Such resolution-based decision procedures can be obtained by using refinements of resolution such as ordered resolutionn with selection, or ordered chaining with selection.