PaMpeR: proof method recommendation system for Isabelle/HOL
PaMpeR: proof method recommendation system for Isabelle/HOL
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 …