Hi, I'm learning HOL tactics and started to gather relevant literature. Myreen's Guide to HOL4 interaction and basic proofs
https://hol-theorem-prover.org/HOL-interaction.pdf gives a little introduction to tactics and http://www.cs.uu.nl/docs/vakken/pv/resources/kananaskis-7-quick.pdf gives a cheat sheet for tactics and other things. Thomas Tuerk's Interactive Theorem Proving Course https://hol-theorem-prover.org/hol-course.pdf has Part VIII on basic tactics. There is the 4th chapter of the DESCRIPTION and of course the REFERENCE gives a full account on tactics as well. https://arxiv.org/abs/1804.00595 Thibault Gauthier <https://arxiv.org/search/cs?searchtype=author&query=Gauthier%2C+T>, Cezary Kaliszyk <https://arxiv.org/search/cs?searchtype=author&query=Kaliszyk%2C+C>, Josef Urban <https://arxiv.org/search/cs?searchtype=author&query=Urban%2C+J> Learning to Reason with HOL4 tactics automates the selection of HOL tactics What else do you recommend to read on HOL tactics, on using and writing them? - Gergely
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
