Main Page | See live article | Alphabetical index HOL is an abbreviation for Higher order logic, a branch of symbolic logic in which statements can be quantified over objects, predicates, predicates of predicates etc. There is also a theorem prover called HOL; see HOL theorem prover. This article is from Wikipedia. All text is available under the terms of the GNU Free Documentation License.