Dear ProofPower users,

I have written an extensive glossary of HOL terminology, suitable for
those wishing to understand basic concepts about the HOL logic and how
HOL theorem provers work.  It is written as part of the documentation
for the HOL Zero system, but is relevant for all HOL systems and goes
to lengths to explain variant terminology.  As well as basic concepts
about HOL, it also explains various relevant concepts from formal
mathematics, ML programming.  The latest version has around 240
entries, and is available here:

Please feel free to use this for whatever purpose you wish.  I do not
yet consider this work to be closed, and welcome any debate or
feedback about any aspect.  Obvious enhancements, if there is enough
interest, would be to extend to coverage to concepts not used in HOL
Zero (such as "rewriting", "subgoal package", "meson"), and to make it
an HTML file or PDF.

Many thanks to Rob and Roger for helping me with many parts of this

Mark Adams
Proof Technologies Ltd

Proofpower mailing list

Reply via email to