Die Prädikatenlogik erster Stufe als mächtiges Werkzeug der symbolverarbeitenden KI läßt sich mit Hilfe von Theorembeweisern automatisieren. Kurt Gödel hat in den 1930er Jahren den Logikern und KI-Wissenschaftlern gnadenlos die Grenzen der Automatisierung aufgezeigt. Grenzen hat die Logik auch dann, wenn es um die Beschreibung von Unsicherheit geht.