3. Logisches Denken wird automatisch

In der ersten Phase der KI‐Forschung war die Suche nach allgemeinen Problemlösungsverfahren wenigstens in der formalen Logik erfolgreich. Dort wurde ein mechanisches Verfahren angegeben, um die logische Allgemeingültigkeit von Formeln zu beweisen. Das Verfahren konnte auch von einem Computerprogramm ausgeführt werden und leitete in der Informatik das automatische Beweisen ein.

Der Grundgedanke ist einfach zu verstehen. In der Algebra werden Buchstaben x, y, z, … durch Rechenoperationen wie z. B. Addieren (+) oder Subtrahieren (−) verbunden. Die Buchstaben dienen als Leerstellen (Variablen), um Zahlen einzusetzen. In der formalen Logik werden Aussagen durch Variablen A, B, C, … bezeichnet, die durch logische Junktoren wie z. B. „und“ (\( \wedge \)), „oder“ (\( \vee \))‚ „wenn‐dann“ (\( \rightarrow \)), „nicht“ (\( \lnot \)) verbunden werden. Die Aussagenvariablen dienen als Leerstellen, um Aussagen einzusetzen, die entweder wahr oder falsch sind. So ist z. B. A  \( \wedge \) B eine logische Formel, die durch Einsetzung der wahren Aussagen 1 + 3 = 4 für A und 4 = 2 + 2 für B in die wahre Aussage 1 + 3 = 4 \( \wedge \) 4 = 2 + 2 übergeht. In der Arithmetik ergibt sich daraus der wahre Schluss 1 + 3 = 4 \( \wedge \) 4 = 2 + 2 \( \rightarrow \) 1 + 3 = 2 + 2. Allgemein ist aber der Schluss A \( \wedge \) B \( \rightarrow \) C nicht wahr. Demgegenüber ist der Schluss A \( \wedge \) B \( \rightarrow \) A logisch allgemeingültig, da für die Einsetzung von beliebigen wahren oder falschen Aussagen für A und B sich immer eine wahre Gesamtaussage ergibt. ...