Deduktion: von der Theorie zur Anwenduna

摘要

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 Problemloser" 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.