Higher-Order Logic

Higher-Order Logic

m Investigated extensively by Gordon [M. Gordon 85-88].

m HOL mechanized for verification by R. Milner on LCF. LCF implemented in ML (the LCF Meta-language).

m Proof in HOL is achieved by repeatedly applying inference rules to axioms or to previously proved theorems.

Previous slide Next slide Back to the first slide View Graphic Version