3 ms·
I think coq has some kind of ml software. I saw it mentioned in the proof general UI. I'm not sure how good it is
by anonlastname 8y ago
I think coq has some kind of ml software. I saw it mentioned in the proof general UI. I'm not sure how good it is
- chriswarbo 8y agoPossibly this? http://www.macs.hw.ac.uk/~ek19/ML4PG/ http://www.macs.hw.ac.uk/~ek19/ML4PG/ It's mostly in maintenance mode (at least, I seem to have inherited its maintenance; and it's such a horrible mess of Emacs Lisp + Matlab + shell scripts that I don't dare touch it unless asked ;) ). It's used for clustering statements and proofs, the idea being that if you're stuck trying to prove something, you might be able to find something "similar" in an existing library to use as inspiration. It's mostly to help with manual searches, rather than automatically solving anything (although there is some related work on doing that for Coq called SEPIA https://arxiv.org/abs/1505.07987 https://arxiv.org/abs/1505.07987 and ACL2 http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html ).