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

Reply via email to