Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method

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.

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Sean McLaughlin, Frank Pfenning
• Keywords: Automated Reasoning, CADE 2009, Intuitionistic Theorem Provers, Non-classical Logics, Recursive Backward Subsumption