Efficient Implementation of the Inverse Method for First-Order Intuitionistic Logic

This paper contains the results of the research related to Maslov’s inverse method and its application to first-order intuitionistic logic. Several proof search strategies for the inverse-method intuitionistic calculus, which allow reducing the proof search space and avoiding redundant inferences, are proposed and explained in detail. Some strategies are new, others are adapted variants of the existing strategies for classical logic. This article includes a detailed description of the automated theorem-proving system WhaleProver for first-order intuitionistic logic, which is based on the inverse method. This article also describes the experimental comparison of the proposed proof search strategies and comparison of WhaleProver with other first-order intuitionistic logic provers. For problems from the ILTP benchmark library, WhaleProver shows comparable results with state-of-the-art intuitionistic provers (ileanCoP, Imogen). Moreover, WhaleProver solves new problems from ILTP, in comparison with all other provers. The results of the study show that inverse method implementation can be at least as efficient as state-ofthe-art implementations of other theorem-proving methods (e.g., tableaux methods).