Prädikatenlogik höherer Stufe

Unter Logik höherer Stufe (englisch: Higher-Order Logic, HOL) versteht man eine Erweiterung der Prädikatenlogik erster Stufe. Sie basiert auf dem typisierten Lambda-Kalkül und geht auf Alonzo Churchs Theory of Simple Types zurück.

Entwickelt um 1940 als ein Versuch der Formalisierung der Logik in der Principia Mathematica von Whitehead und Russell, ist sie von Leon Henkin und Peter Andrews eingehend untersucht worden. Anfang der 1970er Jahre wurden nicht-klassische Versionen der Logik höherer Stufe entwickelt, die die Grundlage der modernen Typtheorie (Peter Martin-Löf, Jean-Yves Girard) und Beweistheorie (Girard, Huet, Harper, Honsell) bilden. Da die Logik höherer Stufe sowohl mächtig als auch relativ einfach auf einem Computer zu implementieren ist, wurden in letzter Zeit einige Theorembeweiser hierfür entwickelt, die gleichermaßen für die Mathematik als auch für die Informatik von Interesse sind.

Siehe auch

• Formale Methode

Literatur

• Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, 1986.
• J. Lambek, P.J Scott: Introduction To Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK, 1986. [1]

Weblinks

• Herbert B. Enderton: „Second-order and Higher-order Logic“ in der Stanford Encyclopedia of Philosophy (englisch, inklusive Literaturangaben)