Higher Order Logic (1) A logical system, usually a Type Theory, with multiple ranges of quantification (usually called types) some of which contain sets or functions. See also: Church's Simple Theory of Types, Pure Type System Higher Order Logic (2) A proof tool, originally developed by the Hardware Verification Group at The University of Cambridge Computer Laboratories. Now available as several variants (HOL88, HOL90, HOL98, HOL Light), supporting the construction and checking of proofs in Higher Order Logic. There are also many more proof tools for variants of Higher Order Logic or for logical Type Theories which do not go under the name "HOL". There is an annual international workshop concerned with the development and application of these proof tools. hyper-rational An exacting standard of rationality based on the assertion only of formally proven analytic propositions.