Theorem Prover for Intuitionistic Logic Based on the Inverse Method
- Authors: Pavlov V.A.1, Pak V.G.1
-
Affiliations:
- Peter the Great St.Petersburg Polytechnic University
- Issue: Vol 44, No 1 (2018)
- Pages: 51-61
- Section: Article
- URL: https://journals.rcsi.science/0361-7688/article/view/176579
- DOI: https://doi.org/10.1134/S036176881801005X
- ID: 176579
Cite item
Abstract
The first-order intuitionistic logic is a formal theory from the family of constructive logics. 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). Owing to this feature, intuitionistic logic has many applications in mathematics and computer science. Many modern proof assistants include automated tactics for the first-order intuitionistic logic, which simplify the task of solving challenging problems, such as formal verification of software, hardware, and protocols. In this paper, a new theorem prover (called WhaleProver) for full first-order intuitionistic logic is presented. Testing on the ILTP benchmarking library has shown that WhaleProver performance is comparable with the 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. It is also described how to adopt for this calculus several existing proof search strategies proposed for different logical calculi by S.Yu. Maslov, V.P. Orevkov, A.A. Voronkov, and others. In addition, a new proof search strategy is proposed that allows one to avoid redundant inferences. The paper includes results of experiments with WhaleProver on the ILTP library. We believe that Whale- Prover can be used as a test bench for different inference procedures and strategies, as well as for educational purposes.
About the authors
V. A. Pavlov
Peter the Great St.Petersburg Polytechnic University
Author for correspondence.
Email: vlapav239@gmail.com
Russian Federation, ul. Politekhnicheskaya 29, St.Petersburg, 195251
V. G. Pak
Peter the Great St.Petersburg Polytechnic University
Email: vlapav239@gmail.com
Russian Federation, ul. Politekhnicheskaya 29, St.Petersburg, 195251