The printed manual [Gordon and Melham, 1993, pp. 191–232] (ISBN: 0-521-44189-7)
is the definite source:
Part III: The HOL Logic [Gordon and Melham, 1993, pp. 191–232]. “Part III
presents the logic supported by HOL (‘The HOL Logic’). It consists of two
chapters: an informal introduction and a formal set-theoretic semantics
(written by Andrew Pitts).” [Gordon and Melham, 1993, p. xv] In an email to the
author, Andrew Pitts confirmed that originally he wrote the material in the
file available online, which contains both (!) chapters.
http://owlofminerva.net/files/fom_2018.pdf
<http://owlofminerva.net/files/fom_2018.pdf> (direct link), footnote 2
http://doi.org/10.4444/100.111 <http://doi.org/10.4444/100.111>
(persistent link)
An updated version is available for download at:
http://sourceforge.net/projects/hol/files/hol/kananaskis-13/kananaskis-13-logic.pdf
<http://sourceforge.net/projects/hol/files/hol/kananaskis-13/kananaskis-13-logic.pdf>
For terms see pp. 17 ff. (section 1.3).
As mentioned earlier, I would propose to make the most recent PDF file
accessible online (without having to download) at a link such as:
https://hol-theorem-prover.org/logic.pdf
<https://hol-theorem-prover.org/logic.pdf>
Kind regards,
Ken Kubota
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
> Am 08.11.2019 um 16:48 schrieb Miranda, Brando <[email protected]>:
>
> Hi,
>
> This is my first message to the HOL list so hope its not out of the rules for
> the list (couldn’t find the rules).
>
> I wanted to find the formal grammar for generating terms (formulas) in HOL
> (Light). I was wondering were I could find such a specification?
>
>
> Thanks!
>
> Brando
>
>
>
>
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
