Unter Deduktion versteht man die Herleitung logischer Konsequenzen aus einer gegebenen Menge
logischer Axiome. In den Anfängen der formalen Logik bestand die Hoffnung, dass Deduktion
auch für ausdrucksstarke Logiken, die alles mathematische Wissen axiomatisieren können, voll
automatisierbar ist und damit mathematische Theoreme nicht mehr mühsam vom Menschen bewiesen
werden müssen, sondern ein Deduktionsverfahren
bei Eingabe des Theorems einfach entscheidet, ob
dieses aus der Axiomenmenge folgt oder nicht.
Erste Unentscheidbarkeitsresultate machten dann
aber die Hoffnung auf eine vollständige Automatisierung der Mathematik zunichte. Entsprechendes
gilt für die Hoffnung, nichttriviale semantische Eigenschaften von Programmen (wie Terminierung,
Korrektheit bzgl. einer formalen Spezifikation) zu
entscheiden oder künstliche Intelligenz dadurch zu
realisieren, dass man alles wichtige Wissen über die
Welt axiomatisiert und dann einen ,,allgemeinen
Problemlöser“ einsetzt, der daraus Schlüsse zieht.
Für partiell-entscheidbare Logiken (wie die wichtige Prädikatenlogik erster Stufe) kann man aber
mit einem partiellen Entscheidungsverfahren für
gültige Aussagen (d. h. Aussagen, die tatsächlich
aus der Axiomenmenge folgen) stets in endlicher
Zeit feststellen, dass dies der Fall ist. Automatische
Theorembeweiser sind im Prinzip solche partiellen Entscheidungsverfahren. Es stellte sich aber
zunächst heraus, dass mit diesen nur sehr triviale mathematische Theoreme vollautomatisch
bewiesen werden können. Zur Lösung dieses Problems wurden hier drei verschiedene Strategien
verfolgt, die sich alle in geeigneten Anwendungsbereichen als erfolgreich herausstellten. Zum einen
wurde die Effizienz von automatischen Beweisern durch Verbesserung der zugrunde liegenden
Theorie, aber auch durch ausgefeilte Implementierungstechniken, erheblich verbessert. Zum
anderen ging man bei der interaktiven Deduktion
dazu über, den Menschen in den Beweisprozess
mit einzubeziehen. Schließlich suchte man, für
auf spezielle Anwendungsprobleme angepasste
ausdrucksschwächere Logiken, nach effizienten
Entscheidungsverfahren. Im Folgenden gehen
wir auf Erfolge dieser drei Ansätze exemplarisch
ei