WhaleProver: First-order intuitionistic theorem prover based on the inverse method

Abstract

The first-order intuitionistic logic is a formal theory from the family of constructive theories. In intuitionistic logic, it is possible to extract a particular example x= a and a proof of a formula P(a) from a proof of a formula ∃xP(x). Thanks to this feature, intuitionistic logic has many applications in mathematics and computer science. Several modern proof assistants include automated tactics for the first-order intuitionistic logic which could simplify the task of solving challenging problems, e.g. formal verification of software, hardware, and protocols. In this article, we present a new theorem prover (named WhaleProver) for full first-order intuitionistic logic. Testing on the ILTP benchmarking library has shown that WhaleProver performance is comparable with state-of-the-art intuitionistic provers. Our prover has solved more than 800 problems from the ILTP version 1.1.2. Some of them are intractable for other provers. WhaleProver is based on the inverse method proposed by S. Yu. Maslov. We introduce an intuitionistic inverse method calculus which is in turn a special kind of sequent calculus. Then, we describe how to adopt for this calculus several existing proof search strategies which were proposed for different logical calculi by S. Yu. Maslov, V.P. Orevkov, A.A. Voronkov, and other authors. In addition, we suggest new proof search strategy that allows avoiding redundant inferences. This article includes results of experiments with WhaleProver on the ILTP library. We believe that WhaleProver can be used further as a test bench for different inference procedures and strategies, as well as for educational purposes.