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 <miran...@illinois.edu>: > > 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
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info