file.pdf (221.11 kB)
0/0

Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method

Download (221.11 kB)
journal contribution
posted on 01.08.2013 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

History

Publisher Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/s10703-013-0195-3

Date

01/08/2013

Exports

Exports