HOL4 Description Manual provides a detailed description of available tactics.
http://sourceforge.net/projects/hol/files/hol/kananaskis-12/kananaskis-12-description.pdf/download -Umair On Tue, Mar 5, 2019 at 11:09 AM Gergely Buday <gbu...@gmail.com> wrote: > 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 >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
