Proof-Pattern Recognition and Lemma Discovery in ACL2

Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson +1

We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathe…