Saint-Petersburg State Polytechnic University, Russia

Maslov's inverse method is a local proof search procedure that is applicable to a wide range of logical calculi. We present an overview of the inverse method for theorem proving in first-order logic. We discuss existing modifications of the inverse method, connections between this method and popular first-order theorem proving techniques: resolution and tableau methods. We also give a brief survey of the inverse method implementations for other logical calculi, as modal logics and intuitionistic logic. This paper includes a description of our computer program for automated theorem proving in first-order logic using the inverse method. We discuss important details of our implementation, and present test results on problems from different scientific fields.