Output details
11 - Computer Science and Informatics
University of Dundee
Proof-Pattern Recognition and Lemma Discovery in ACL2
<11> The paper proposes a pioneering method to combine statistical and symbolic machine-learning techniques to process big libraries of computer proofs and discover new lemmas. The publication also presents full implementation of this method as ACL2(ml) programming environment. The work is a result of collaboration between Dundee, Edinburgh and Chalmers, funded by Komendantskaya’s First Grant (EP/J014222/1,£120K), as well as EPSRC EP/H024204/1, £514K and ERC Marie Curie, £200K. The significance of the results has been acknowledged by SICSA Industrial Proof of Concept grant (PI Komendantskaya) with partners the leading Formal-methods industries Centaur Technologies and Rockwell Collins.