205 citations · 525 across the 28 of their papers we have counts for
3 papers · 2 filters
ACL2(ml): Machine-Learning for ACL2
Jónathan Heras, Ekaterina Komendantskaya
ACL2(ml) is an extension for the Emacs interface of ACL2. This tool uses machine-learning to help the ACL2 user during the proof-development. Namely, ACL2(ml) gives hints to the us…
HoTT formalisation in Coq: Dependency Graphs \& ML4PG
Jónathan Heras, Ekaterina Komendantskaya
This note is a response to Bas Spitter's email of 28 February 2014 about ML4PG: "We (Jason actually) are adding dependency graphs to our HoTT library: https://github.com/HoTT/HoTT/…
Proof Pattern Search in Coq/SSReflect
Jónathan Heras, Ekaterina Komendantskaya
ML4PG is an extension of the Proof General interface, allowing the user to invoke machine-learning algorithms and find proof similarities in Coq/SSReect libraries. In this paper, w…