Sciweavers

Share
CADE
2009
Springer

Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method

10 years 17 days ago
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.
Sean McLaughlin, Frank Pfenning
Added 23 Nov 2009
Updated 23 Nov 2009
Type Conference
Year 2009
Where CADE
Authors Sean McLaughlin, Frank Pfenning
Comments (0)
books