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 aware) by a parser generator.
http://www.proof-technologies.com/holzero/
Mark.
On 09/11/2019 15:48, Petros Papapanagiotou wrote:
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 Light term structure as it is defined here:
https://github.com/jrh13/hol-light/blob/a1ca1f31539c8e9bd40d324c14951e3c76836787/fusion.ml#L99
Hope this helps!
Regards,
Petros
On 08/11/2019 15:48, Miranda, Brando wrote:
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-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Dr. Petros Papapanagiotou
Chancellor's Fellow in Digital Technologies
CISA, School of Informatics, The University of Edinburgh
Academic Coordinator
IoT Research & Innovation Service
http://homepages.inf.ed.ac.uk/ppapapan/
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
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
