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
Michael
From: "Miranda, Brando"
Date: Saturday, 9 November 2019 at 02:50
To: hol-info
Subject: [Hol-info] grammar for HOL Light terms
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 gra
And for HOL Zero there is Appendix C of the User Manual that gives a
formal grammar of the HOL Zero concrete syntax. Again, this is fairly
similar to HOL Light's and HOL4's, but there are numerous small
differences. Note that the formal grammar hasn't actually been checked
(as far as I'm
Hi Brando,
The HOL4 description manual has quite a bit of information, a lot of
which is shared with HOL Light:
http://sourceforge.net/projects/hol/files/hol/kananaskis-13/kananaskis-13-description.pdf/download
I am not sure if there is a similar document for HOL Light.
You can see the HOL
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
