HOL
Axioms
Encoding forall ``\x P(x) = \x true` is saying that the predictae p is always true.
HOL
HOL4 https://kth-step.github.io/itppv-course/
HOL light
- wikpedia
- Harrison’s page
- tutorial quite good
- Thomas Hale - Formal Proof article Succinct summary of axioms
- #
Isabelle
from lcf to isabelle sel4 - verified microkernel
Metalevel is a syntax for describing inference rules
!! x.
\Lambda Universal variables at the meta level. enables Schema==>
is inference rule%x.
is meta level lambda?
Sledgehammer: some history, some tips isabelle cookboook: programming in ML more isabelle ML programming notes
Isabelle => vs –> vs ==> => is the function type –> is implication ==> is meta implication, which is something like a sequent |-