Higher-order logic

Under the logic of a higher level (English Higher -Order Logic, HOL ), also stage logic, understood as an extension of first-order predicate logic. It is based on the typed lambda calculus and goes back to Alonzo Church's Theory of Simple Types.

Developed in 1940 as an attempt to formalize the logic in the Principia Mathematica of Whitehead and Russell, it has been thoroughly examined by Leon Henkin and Peter Andrews. Early 1970s were non-classical versions of the logic of a higher level developed the basis of modern type theory ( Per Martin- Löf, Jean -Yves Girard ) and evidence theory (Jean -Yves Girard, Gérard Huet, Robert Harper, Furio Honsell ) form. Since the logic of a higher level is also relatively easy to implement on a computer powerful than both, some theorem provers have been developed for this purpose lately that are both for mathematics and for the computer science of interest.