Re: [Hol-info] grammar for HOL Light terms

[Ken K. <ma...@ke...>]

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 <mir...@il...>:
> 
> 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
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info