Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-02959-2_19 | CADE |
Keywords | Field | DocType |
non-classical logic,iltp problem library,logics satisfying cut elimination,first-order intuitionistic logic,existing intuitionistic theorem provers,general architecture,efficient implementation,generic proof search procedure,implementation imogen,efficient intuitionistic theorem proving,polarized inverse method,rule subsumption,satisfiability,intuitionistic logic,first order,non classical logic,theorem proving | Theorem provers,Intuitionistic logic,Atomic formula,Discrete mathematics,Proof search,Computer science,Automated theorem proving,Inverse method,Algorithm,Rule of inference,Recursion | Conference |
Volume | ISSN | Citations |
5663 | 0302-9743 | 8 |
PageRank | References | Authors |
0.66 | 13 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sean McLaughlin | 1 | 140 | 9.39 |
| Frank Pfenning | 2 | 3376 | 265.34 |