Higher-Order Logic
Higher-Order Logic
m Extension of FOL that allows variables to range over functions and predicates.
m Unrestricted HOL suffers from a number of paradoxes (e.g. Russell's Paradox). Type theory & a type hierarchy can avoid these problems.
m First user by Hanna in the VERITAS system [Hanna, et. al. 86]