PaMpeR: proof method recommendation system for Isabelle/HOL

Abstract

Deciding which sub-tool to use for a given proof state requires expertise specific to each interactive theorem prover (ITP). To mitigate this problem, we present <pre>PaMpeR</pre>, a <U>p</U>roof <U>m</U>ethod <U>r</U>ecommendation system for Isabelle/HOL. Given a proof state, <pre>PaMpeR</pre> recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. <pre>PaMpeR</pre> generates these recommendations based on existing hand-written proof corpora, thus transferring experienced users' expertise to new users. Our evaluation shows that <pre>PaMpeR</pre> correctly predicts experienced users' proof methods invocation especially when it comes to special purpose proof methods.

Locations

• arXiv (Cornell University) - View - PDF