This is a very minimalistic theorem proving environment that prioritises simple foundations over heavy tooling. It is also based on a very different formal system than Lean/Rocq/etc. which are based on type theory.
Note that “light”, at least in terms of foundations, is not an exaggeration: https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations . This means that everything is encoded in terms of equality: as noted in the tutorial (section 5.3), “p && q” is implemented as “(p, q) = (T, T)”; you can further extend this with “p || q” as “not (not p && not q)” and thus “((p = F, q = F) = (T, T)) = F”.
This is a very minimalistic theorem proving environment that prioritises simple foundations over heavy tooling. It is also based on a very different formal system than Lean/Rocq/etc. which are based on type theory.
Note that “light”, at least in terms of foundations, is not an exaggeration: https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations . This means that everything is encoded in terms of equality: as noted in the tutorial (section 5.3), “p && q” is implemented as “(p, q) = (T, T)”; you can further extend this with “p || q” as “not (not p && not q)” and thus “((p = F, q = F) = (T, T)) = F”.
score 1 · canonical