lick, wählerischer  Die Pioniere, die Ende der 1950er Jahre die ersten Programme für automatisches Beweisen schufen, verfolgten äußerst ehrgeizige Ziele. Einige von ihnen glaubten, in wenigen Jahren seien solche Programme in der Lage, nicht nur einfache Beweise wie den oben beschriebenen, sondern auch sehr komplizierte Beweise zu konstruieren, so dass sie auf diesem Gebiet dem Menschen sogar überlegen wären. Solche Projekte sind inzwischen aufgegeben worden, zumindest vorläufig. Selbst wenn einige Programme theoretisch in der Lage sind, komplizierte Beweise zu finden, brauchen sie dafür unglaublich viel Zeit, da die Zahl der zu prüfenden Möglichkeiten mit der Komplexität der Beweise exorbitant ansteigt. Und wenn die benötigte Zeit das Alter des Universums (oder auch nur einige Wochen) übersteigt, sind solche Programme ohne jedes praktische Interesse.

Paradoxerweise sagt uns dieser Fehlschlag einiges über die Funktionsweise unseres eigenen Verstandes. Wir sind dem Computer nicht etwa deshalb beim Beweisen überlegen, weil wir die Deduktionsregeln besser anzuwenden vermögen, sondern weil wir aus der Vielzahl der möglichen Ableitungen einige wenige auswählen und die Übrigen unberücksichtigt lassen, so dass die Zahl der zu prüfenden Möglichkeiten sich in Grenzen hält. Die Methoden, mit denen wir diese Auswahl vornehmen, sind noch weitgehend unbekannt.    - (thes)