Machine Learning for ACL2

Summary:

We present ACL2(ml), an extension for Emacs to find families of related ACL2 definitions and proofs on the basis of shape of terms.

---

Related papers (ordered from newer to older):

• J. Heras and E. Komendantskaya. ACL2(ml): Machine-Learning for ACL2. Proceedings ACL2 Workshop 2014.
• J. Heras, E. Komendantskaya, M. Johansson, and E. Maclean. Proof-Pattern Recognition and Lemma Discovery in ACL2. Proceedings LPAR-19. LNCS 8312, pp. 389-406. 2013.
• J. Heras, E. Komendantskaya, M. Johansson, and E. Maclean. Extended version of the paper Proof-Pattern Recognition and Lemma Discovery in ACL2.

Related talks (ordered from newer to older):

• A talk in the Scottish Theorem Proving Seminar. St Andrews, 31 January 2014.

Related documents:

• Description of the project.
• Manual.
• Clusters found in the ACL2 repository using ACL2(ml).

---

Requirements to install ACL2(ml) v.2.:

• Emacs.
• ACL2.

Download

• ACL2(ml).

Installation

After downloading ACL2(ml), unzip the file and follow the instructions of the user manual.

---

Requirements to install ACL2(ml) v.1. (LPAR version):

• Emacs.
• ACL2.
• OCaml (optional, but it is necessary for the automatic generation of auxiliary lemmas).

Download

• ACL2(ml).

Installation

After downloading ACL2(ml), unzip the file and follow the instructions of the user manual.

---

Contact

Please address any queries about ACL2(ml) to joheras at gmail.com