The Inverse Method Application for Non-Classical Logics

Abstract

Maslov’s inverse method is an automated theorem proving method: it can be used to develop computer programs that prove theorems automatically (such programs are called theorem provers). The inverse method can be applied to a wide range of logical calculi: propositional logic, first-order logic, intuitionistic logic, modal logics etc. We give a brief historical background of the inverse method, then discuss existing modifications and implementations of the inverse method for non-classical logics (intuitionistic logic, modal logics and some other logics). We introduce a variant of the inverse method for intuitionistic logic - a logic that allows only constructive proofs, i.e. proofs that construct an existing mathematical object instead of just establishing the fact that such an object exists. In short, intuitionistic logic can be seen as classical logic without the law of excluded middle A ∨ ¬A or the law of double negation elimination ¬¬A ⊃ A. So, classical proofs by contradiction are not allowed in intuitionistic logic. We discuss our experimental program implementation of the inverse method for intuitionistic logic: some details of implementation, results of experiments on ILTP problems (ILTP is a common library of test problems for intuitionistic theorem provers).