I have written an extensive glossary of HOL terminology (see attached text file), for those wishing to understand the HOL logic and how theorem provers work. It forms part of the documentation of my forthcoming HOL Zero theorem prover, which is free and open source. Please feel free to use this for whatever purpose you wish. I would be most grateful for any feedback anyone has.
It defines about 180 concepts relevant to basic HOL system usage (e.g. "quotation", "fixity", "variable capture") and implementation (e.g. "preterm", "LCF-style", "lexical analysis"), together with some relevant background in ML programming and formal mathematics (e.g. "abstract datatype", "formal language"). It aims to reflect consensus usage in the HOL community, although there are a few notable revisions (e.g. "abstraction term", "assertion") and a few new concepts (e.g. "language kernel", "proof auditing"). It does not aim to cover non-basic aspects of HOL theorem proving that are not used in HOL Zero (e.g. "rewriting", "subgoal package", "meson"), although maybe I could produce a general HOL version if there is enough interest. Mark Adams
GLOSSARY.gz
Description: GNU Zip compressed data
------------------------------------------------------------------------------ Beautiful is writing same markup. Internet Explorer 9 supports standards for HTML5, CSS3, SVG 1.1, ECMAScript5, and DOM L2 & L3. Spend less time writing and rewriting code and more time creating great experiences on the web. Be a part of the beta today. http://p.sf.net/sfu/beautyoftheweb
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
