file.pdf (221.11 kB)

Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method

Download (221.11 kB)
journal contribution
posted on 01.08.2013, 00:00 by Sean McLaughlin, Frank Pfenning
The inverse method is a generic proof search procedure applicable to non-classical logics satisfying cut elimination and the subformula property. In this paper we describe a general architecture and several high-level optimizations that enable its efficient implementation. Some of these rely on logic-specific properties, such as polarization and focusing, which have been shown to hold in a wide range of non-classical logics. Others, such as rule subsumption and recursive backward subsumption apply in general. We empirically evaluate our techniques on first-order intuitionistic logic with our implementation Imogen and demonstrate a substantial improvement over all other existing intuitionistic theorem provers on problems from the ILTP problem library


Publisher Statement

The final publication is available at Springer via