PMRS

Proof Method Recommendation System wiki page

PMRS is a machine learning based tool dedicated to help engineers when they try to work towards a proof goal. Currently it has two major components.

One is the feature extraction component, which is capable of generating bool style feature from a current proof state, and write them in a file by default in ~/.isabelle folder.

User can define their own feature extraction and add it to the existing feature list by modifying Assertion.ML

To use the extraction system on large corpora, you need to follow the instructions in FE_Interface.ML comments.

The other part is the actual proof method recommendation system. By typing keyword "Proof_Advice" user can obtain recommendation from the output. The keyword does not change anything in the proof state but output the recommendation. Argument recommendation is the next step of development.