Intellectual Systems and Technologies

An experimental computer program for automated reasoning in intuitionistic logic using the inverse method

V. A. Pavlov, V. G. Pak

Peter the Great Saint-Petersburg Polytechnic University

Abstract: We discuss the inverse method of automated theorem-proving that was invented by S. Maslov. The inverse method can be applied to various logics: propositional logic, first-order logic, modal logics, intuitionistic logic, etc. In the current article, we present an overview of the key publications on the inverse method, describe in detail an inverse method calculus for first-order intuitionistic logic. We propose adapted as well as original optimizing strategies for the developed calculus. We discuss a proof search algorithm for the proposed calculus and our program implementation named WhaleProver. We compare WhaleProver with state-of-the-art intuitionistic theorem provers on problems from the ILTP library, which is a common benchmarking library for testing intuitionistic theorem provers.

Keywords: automated theorem proving, sequent calculus, inverse method, intuitionistic logic, ILTP.

UDC: 004.832.32

DOI: 10.5862/JCSTCS.234.7