Re: [Hol-info] literature for tactics

[Umair Siddique]

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  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
> , Cezary
> Kaliszyk
> , Josef
> Urban 
> 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

[Hol-info] literature for tactics

[Gergely Buday]

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
, Cezary
Kaliszyk ,
Josef Urban 
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