Logik für Informatiker

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 Martin Kreuzer
Stefan Kühling

Logik für Informatiker

Higher Education
München • Harlow • Amsterdam • Madrid • Boston
San Francisco • Don Mills • Mexico City • Sydney
a part of Pearson plc worldwide

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 Bibliografische Information der Deutschen Nationalbibliothek

Die Deutsche Nationalbibliothek verzeichnet diese Publikation in der Deutschen

Nationalbibliografie;
detaillierte bibliografische Daten sind im Internet über <[Link] abrufbar.

Die Informationen in diesem Buch werden ohne Rücksicht auf einen eventuellen Patentschutz
veröffentlicht. Warennamen werden ohne Gewährleistung der freien Verwendbarkeit benutzt.
Bei der Zusammenstellung von Texten und Abbildungen wurde mit größter Sorgfalt
vorgegangen. Trotzdem können Fehler nicht ausgeschlossen werden. Verlag, Herausgeber und
Autoren können für fehlerhafte Angaben und deren Folgen weder eine juristische
Verantwortung noch irgendeine Haftung übernehmen. Für Verbesserungsvorschläge und
Hinweise auf Fehler sind Verlag und Herausgeber dankbar.
Es konnten nicht alle Rechteinhaber von Abbildungen ermittelt werden. Sollte dem Verlag
gegenüber der Nachweis der Rechtsinhaberschaft geführt werden, wird das branchenübliche
Honorar nachträglich gezahlt.
Alle Rechte vorbehalten, auch die der fotomechanischen Wiedergabe und der Speicherung in
elektronischen Medien. Die gewerbliche Nutzung der in diesem Produkt gezeigten Modelle
und Arbeiten ist nicht zulässig.
Fast alle Hardware- und Softwarebezeichnungen und weitere Stichworte
und sonstige Angaben, die in diesem Buch verwendet werden,
sind als eingetragene Marken geschützt.
Da es nicht möglich ist, in allen Fällen zeitnah zu ermitteln,
ob ein Markenschutz besteht, wird das ® Symbol in diesem Buch nicht verwendet.

10 9 8 7 6 5 4 3 2

12

ISBN 978-3-8273-7215-4 (Buch)

ISBN 978-3-86326-739-1 (E-Book)


c 2006 by Pearson Deutschland GmbH
Martin-Kollar-Straße 10–12, D-81829 München/Germany
Alle Rechte vorbehalten
[Link]
A part of Pearson plc worldwide

Programmleitung: Birger Peil, bpeil@[Link]

Korrektorat: Brigitta Keul, München
Einbandgestaltung: Thomas Arlt, tarlt@[Link]
Herstellung: Monika Weiher, mweiher@[Link]
Satz: le-tex publishing services GmbH, Leipzig
Druck und Verarbeitung: GraphyCems, Villatuerta

Printed in Spain

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 Inhaltsverzeichnis

Vorwort 7

Kapitel 1 Was ist Logik? 13

1.A Logische Systeme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.B Anwendungen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

Kapitel 2 Aussagenlogik 19
2.A Grundlagen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.B Das Resolutionskalkül der Aussagenlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

Kapitel 3 Hornlogik 41
3.A Grundlagen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.B Das Resolutionskalkül der Hornlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
3.C Logik-Programmierung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

Kapitel 4 Prädikatenlogik 59
4.A Grundlagen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
4.B Normalformen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.C Die Unentscheidbarkeit der Prädikatenlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.D Das Resolutionskalkül der Prädikatenlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99

Kapitel 5 Gleichungslogik 105

5.A Termersetzungssysteme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.B Die Knuth-Bendix-Vervollständigung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128

Kapitel 6 Modallogik 133

6.A Grundlagen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135
6.B Das Tableaukalkül der Aussagenlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142
6.C Das modallogische Tableaukalkül . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148
Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154

Kapitel 7 Temporallogik 159

7.A Zeitlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
7.B Der until-Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 INHALTSVERZEICHNIS

Kapitel 8 Weitere logische Systeme 183

8.A Dynamische Logik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
8.B Prozesslogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189
8.C Intuitionistische Logik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193
Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200

Kapitel 9 Hilbert-Kalküle 203

9.A Die axiomatische Beschreibung logischer Systeme . . . . . . . . . . . . . . . . . . . . . . . . 204
9.B Vollständigkeit und Korrektheit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209
Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215

Anhang Tipps zu den Übungsaufgaben 221

Symbolverzeichnis 235

Literaturverzeichnis 239

Sachregister 241

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 Vorwort

Das Lügner-Paradoxon
Wenn du sagst, du lügst,
und du sprichst die Wahrheit,
dann lügst du.
(Eubulides, 4. Jhd. v. Chr.)

Dieses Buch basiert auf der Vorlesung „Logik für Informatiker“, die der erste Autor
seit 2002 regelmäßig an der Universität Dortmund hält. Das inhaltliche Grundgerüst
dieser Vorlesung, das von den Professoren des Fachbereichs Informatik vorgeschlagen
worden war und auch die Basis dieses Buches darstellt, verfolgt die Idee, diejenigen
Teilbereiche der mathematischen Logik zu behandeln, die für die moderne Informatik
relevant bzw. nützlich sind.

Warum ein Buch zur „Logik für Informatiker“?

Bücher mit dem Titel „Logik für Informatiker“ (o. Ä.) gibt es bereits eine ganze Reihe.
Die meisten von ihnen wurden entweder von mathematischen Logikern oder ein-
schlägig forschenden theoretischen Informatikern geschrieben.
Wie kommen ein Computeralgebraiker und ein Student auf die Idee, dieses wohl-
bestellte Feld zu beackern? Zum einen hatten wir als Neulinge vor ein paar Jahren
dasselbe Problem, vor dem auch viele Informatik-Studenten stehen: Die mathemati-
sche Logik erscheint auf den ersten Blick als ein staubtrockenes, schwer zugängliches
und wenig verlockendes Gebiet. Zum anderen haben wir uns, da wir nicht tagtäglich
damit arbeiten, noch nicht an abschreckende Terminologien oder abstruse Notatio-
nen gewöhnt, die sich von dem in der Mathematik üblichen oft stark unterscheiden.
Wir haben daher versucht, diese Einführung in die mathematische Logik möglichst
ansprechend und allgemein verständlich zu gestalten. Wir haben nach selbst erklä-
renden Bezeichnungen gesucht und die Zahl der Spezialsymbole so gering wie mög-
lich gehalten. Algorithmen beschreiben wir nicht mit Pseudocode, sondern mit deut-
schen Sätzen. Statt formal korrekter, aber umständlicher Formelsprache verwenden
wir einen mehr verbalen Stil, der mangelnde Exaktheit durch leichte Zugänglichkeit
und einen gelegentlichen Schuss Humor kompensieren soll. Wir hoffen, dass diese
Vorgehensweise den Zorn der Experten nicht allzu sehr erregt. Gleichzeitig wissen wir
jedoch aus Erfahrung, dass dieser Stil bei Informatik-Studenten im Grundstudium gut
ankommt und didaktisch erfolgreich ist.

Was steht denn nun in diesem Buch drin?

Der Hauptteil dieses Buches beschäftigt sich mit logischen Systemen, die für die In-
formatikausbildung im Grund- und Hauptstudium von Nutzen sind und eine gewisse
theoretische Grundlage für manche Bereiche der Informatik darstellen. Was wir da-
bei unter einem logischen System verstehen, wird in Kapitel 1 erklärt: eine Syntax,
die festlegt, welche Arten von Formeln man betrachtet, eine Semantik, die uns hilft,
diesen Formeln Wahrheitswerte und somit eine „Interpretation“ oder „Bedeutung“

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 VORWORT

zuzuordnen, und eventuell ein Kalkül, mit dem wir die Unerfüllbarkeit von Formeln
testen können. Die Betonung der Kalküle ist dabei gewollt, denn in unserer anwen-
dungsorientierten Betrachtung der mathematischen Logik spielen sie eine zentrale
Rolle.
In Kapitel 2 beginnen wir dann mit dem prototypischen logischen System, nämlich
der Aussagenlogik, die viele Studenten schon in der Schule kennen gelernt haben. Wir
liefern auch gleich zwei Kalküle für die Aussagenlogik: die Wahrheitstafelmethode
und das klassische Resolutionskalkül. Da beide für praktische Zwecke zu ineffizient
sind, betrachten wir im dritten Kapitel die aussagenlogische Variante der Hornlogik,
wo wir den Markierungsalgorithmus und SLD-Resolutionen anzubieten haben. Dies
erlaubt nebenbei eine kurze Einführung in PROLOG. Hier wie später beschränken wir
uns meist auf die aussagenlogischen Versionen der betrachteten logischen Systeme
und zwar aus zwei Gründen: Einerseits sind diese Versionen für viele Anwendungen
völlig ausreichend und andererseits tritt die Mehrzahl der Hauptideen und -effekte
bereits im aussagenlogischen Fall auf.
Das vierte Kapitel behandelt die Prädikatenlogik. Es ist nicht nur das umfang-
reichste, sondern erfahrungsgemäß auch das schwierigste. Wir behandeln die Her-
brand-Theorie und stellen die Unifikation und das prädikatenlogische Resolutions-
kalkül vor, auch wenn dieses nur ein Semi-Entscheidungsverfahren darstellt. Im fünf-
ten Kapitel untersuchen wir die Gleichungslogik: Termersetzungssysteme und die
Knuth-Bendix-Vervollständigung sind nicht nur Heimspiele für Computeralgebraiker,
sie ergeben manchmal auch ein effizientes Kalkül in gleichungsdefinierten Theorien.
Das Studium der Modallogik in Kapitel 6 nehmen wir zum Anlass, die Wirkungsweise
von Tableaukalkülen zu erläutern. Neben der zeitlogischen Variante der Modallogik
folgen dann die eigentliche Temporallogik in Kapitel 7, die dynamische Logik, die
Prozesslogik und die intuitionistische Logik in Kapitel 8. Den Abschluss bilden die
Hilbert-Kalküle im neunten und letzten Kapitel.

Und wie ist das alles geschrieben?

Bei der Darstellung des Stoffes haben wir uns sehr angestrengt, trockene Aneinan-
derreihungen von Fakten zu vermeiden. Jedes Kapitel beginnt mit einer informellen,
humorvollen, scherzhaften oder augenzwinkernden Einleitung, in die wir gelegent-
liche Hinweise auf das eingestreut haben, was dem Leser blüht. Diese Einleitungen
sind blau hinterlegt und folglich leicht auszumachen.
Eine ganz besondere didaktische Maßnahme ist ebenfalls an der Hinterlegung,
und zwar an der hellblauen augenblicklich zu identifizieren. Es handelt sich um
das so genannte fortlaufende Beispiel, von dem sich in jedem Kapitel mindestens
eines findet. Obwohl sie nicht immer ganz ernst gemeint sind, sollen diese Beispiele
den Leser keineswegs zum Fortlaufen bringen. Nein, sie heißen so, weil sie sich
typischerweise durch das ganze Kapitel ziehen. Die neu eingeführte Theorie wird
an ihnen sofort ausprobiert und durchexerziert. Viele fortlaufende Beispiele sind im
Stile von Übungsaufgaben mit Lösungen gehalten, so dass der Leser bereits Ansätze
und Lösungsmethoden für die späteren Übungen aufnimmt, während er noch das
eigentliche Kapitel verdaut.
Die Lemmata (= Hilfssätze), Sätze, Korollare (= Folgerungen) und Theoreme
(= besonders wichtige, zentrale Sätze) sind nicht viel anders aufgeschrieben als in

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 Vorwort

anderen Mathebüchern auch. Bei den zugehörigen Beweisen versuchen wir, so ele-
mentar wie möglich zu bleiben und hoffen, dass sie halbwegs richtig sind. Einen
wesentlich größeren Wert haben wir jedoch auf die Algorithmen gelegt, wie deren
blaue Hinterlegung bereits andeutet. Aus der Sicht des Informatikers und Anwen-
ders der mathematischen Logik sind die Algorithmen die wesentlichen Ergebnisse
der Theorie – sie verlocken geradezu zu ihrer Implementation.
Den krönenden Abschluss eines jeden Kapitels bilden die Übungsaufgaben. Als
Fachbuchautor ist man stets versucht, die langwierigsten und langweiligsten Rech-
nungen, die stupidesten Beweise (z. B. die allseits beliebte „Induktion über den For-
melaufbau“) und die ekelhaftesten Fallunterscheidungen dem armen Leser aufzubür-
den, und zwar in der Form von so genannten Übungsaufgaben. Zugleich gewinnt man
auf bequeme Weise eine schön lange Liste von Übungsaufgaben. Unserer Erfahrung
nach ist der mit solchen Aufgaben verbundene Lerneffekt minimal. Bei den meisten
Lernenden tritt er überhaupt nicht ein, da sie sich abschrecken lassen und solche
Aufgaben gar nicht erst versuchen. Deswegen haben wir uns der genannten Versu-
chung so gut wir konnten widersetzt. Wir haben uns Übungsaufgaben ausgedacht, die
die Studenten zum Ausprobieren verleiten sollen, die interessant oder witzig wirken
und die den Eindruck vermeiden, die Autoren wären zu faul gewesen, einen Teil
der Theorie selbst auszuarbeiten. Die Geschmäcker sind verschieden und nicht je-
dermanns Humor ist gleich; wir hoffen jedoch, dass sich in unserem bunten Strauß
für jeden Leser ein passendes Blümchen findet. Sollte jemand ausnahmsweise keinen
blassen Schimmer haben, wie man eine bestimmte Aufgabe anpackt, so findet sich
ein (manchmal gar nicht so) kleiner Tipp im Anhang.

Wie bitte? Ein Mathebuch in Farbe?

Jawohl. Wir haben die Möglichkeit einer zweiten Farbe auf vielseitige Weise genutzt:
blaue bzw. hellblaue Hinterlegungen markieren Kapiteleinleitungen, fortlaufende
Beispiele und Algorithmen, Blaue Rahmen markieren die Übungsaufgaben. Und
wenn wir einen Algorithmus in Aktion vorführen (z. B. den Markierungsalgorithmus
in Kapitel 3 oder das Tableaukalkül in Kapitel 6), so kennzeichnen wir bereits abge-
arbeitete Formelteile ebenfalls durch Blaufärbung. Schon rein visuell gleicht dieses
Logik-Buch keinem bisher dagewesenen.

Was bedeutet CWS?

Ganz einfach, CWS bedeutet CompanionWebsite. Und was ist eine Companion Web-
site? Das ist auch ganz einfach. Geben Sie die Adresse [Link]
.de in Ihren Lieblingsinternetbrowser ein und drücken Sie dann auf die Enter-Taste.
 
(Wenn Sie keine Enter-Taste haben, versuchen Sie es mit der Eingabe -Taste oder
der Return-Taste.) Geben Sie in die Suchmaske „Logik für Informatiker“ ein.
Zum einen gibt es weitere Übungsaufgaben in Hülle und Fülle und zwar mit voll-
ständig ausgearbeiteten Lösungen. Zum anderen gibt es weiteres Begleitmaterial, und
für Dozenten gibt es im passwortgeschützten Dozentenbereich auch die kompletten
Lösungen aller Übungsaufgaben des Buches. Zusammengenommen steht das Kürzel
CWS also für über 170 Seiten zusätzlicher Goodies!

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 VORWORT

Ein Wort zur Notation

Die in der mathematischen Logik verwendeten Notationen und Terminologien waren
und sind starken Schwankungen unterworfen. Statt dem Zeichen ∧ verwendete man
früher auch & für die Konjunktion („logisches und“), der Folgepfeil wird wahlweise
mit →, ⊃ oder ⇒ notiert und die Äquivalenzpfeile können in den Gestalten ↔,
≡ und ⇔ materialisieren. Dies führt häufig erfolgreich zur Verwirrung des Lesers,
denn z. B. ≡ bedeutet anderswo die semantische Äquivalenz, das Zeichen ⊃ steht
üblicherweise für „Obermenge“ und einen Pfeil → interpretiert jeder Nicht-Logiker
als Abbildungspfeil. Wie unlogisch! Dazu kommt noch, dass in vielen einschlägigen
Werken Zeichen wie „überladen“ werden, d. h. dass sie je nach Kontext mehrere,
u. U. völlig verschiedene Bedeutungen haben können. Wie sollen wir uns in diesem
Durcheinander zurechtfinden? Wir haben versucht, die Notationen in diesem Buch
nach folgenden Gesichtspunkten zu wählen:
I Zeichen, die im „Rest“ der Mathematik eine eindeutige Bedeutung haben, werden
möglichst nicht „umdefiniert“.
I Gibt es für eine Konstruktion bereits eine in der Mathematik übliche Notation, so
verwenden wir diese, statt eine neue zu erfinden.
I Die Zahl der eingeführten Notationen wird auf das unbedingt Nötige begrenzt.
I Wenn es sich irgendwie vermeiden lässt, werden Symbole nicht „überladen“, d. h.
nicht mit verschiedenen Bedeutungen gebraucht.
Mit der Terminologie ist es ähnlich: Was des einen „Interpretation“ ist, ist des anderen
„Struktur“, der hiesige „Rahmen“ heißt anderswo „Gerüst“, eine „Formel“ hier ist ein
„Ausdruck“ dort, usw. In dieser Lage waren wir bestrebt, Kollisionen mit in anderen
Teilen der Mathematik bereits belegten Begriffen zu vermeiden und haben ansonsten
eine eher zufällige, unseren persönlichen Geschmäckern genehme Auswahl getroffen.
Damit schließen wir diese Ausführungen und wünschen Ihnen ein gutes Verständnis.

Danksagung
An dieser Stelle möchten wir Sie, lieber Leser, nicht mit einigen oberflächlichen
Bemerkungen darüber langweilen, wie viele Menschen zu diesem Buch beigetra-
gen haben. Stattdessen langweilen wir Sie nun mit einer kompletten Liste dieser
Menschen. Eine ganz besondere Erwähnung gebührt Herrn Dr. Peter Ackermann,
der nicht nur jahrelang die Übungen zur Vorlesung „Logik für Informatiker“ betreut
hat, sondern von dem auch viele der Übungsaufgaben in diesem Buch stammen und
der der erfolgreichste Jäger von Fehlern in den verschiedenen Versionen des Manu-
skripts war. Auch unseren weiteren Korrekturlesern Holger Bluhm, Thorsten Camps
und Christian Scholz danken wir herzlich, ebenso wie Hunderten von Dortmunder
Informatik-Studenten, die viele der Übungsaufgaben gelöst und Ungereimtheiten im
Vorlesungsskript aufgedeckt haben.
Es ist klar, dass ein solches Buchprojekt wie das vorliegende nicht ohne die tat-
kräftige Hilfe unserer Familienmitglieder Bettina, Ellen, Heinz, Katharina, Martin und
Veronika möglich gewesen wäre. Wir wissen, dass sich ihre Opfer an gemeinsamer
Freizeit und ihre moralische Unterstützung im Endprodukt widerspiegeln und sind
froh, dass sie sich mit uns darüber freuen. Auch Helmtrud und Rudolf Lohwasser so-
wie Helmut Kreuzer haben uns mit ihrem Faxgerät bzw. E-Mail-Zugang sehr geholfen.

10

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 Vorwort

Ein noch viel direkterer und unmittelbar entscheidender Beitrag zu diesem Projekt
kam vom Team des Verlags Pearson Studium, allen voran von Herrn Marc-Boris Rode.
Wir schätzen uns glücklich, als Autoren eine so professionelle und intensive Betreu-
ung genossen zu haben. Ohne diese Betreuung wäre dieses Buch nie geworden, was es
(hoffentlich) ist: eine etwas andere Einführung in die mathematische Logik – farbig,
lustig, abwechslungsreich und vor allem verständlich. Möge das Lesen Ihnen so viel
Spaß machen wie uns das Schreiben.

Dortmund, März 2006 Martin Kreuzer und Stefan Kühling

11

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 Was ist Logik?

1.A Logische Systeme . . . . . . . . . . . . . . . . . . . . . 14 1

1.B Anwendungen . . . . . . . . . . . . . . . . . . . . . . . . 16

ÜBERBLICK

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 1 WAS IST LOGIK?

Logik ist …
das formale und systematische Studium der Kunst,
Informatik-Studenten zu piesacken. (aus: „Logik für Informatiker und andere
Paradoxa“)

Vor Jahren hielt ich eine Logikvorlesung und begann, wie es sich gehört, mit Aus-
sagenlogik. Zunächst erklärte ich, was man unter einer Aussage versteht: Eine
Aussage ist ein sprachliches Gebilde, das entweder wahr oder falsch ist. Als Bei-
spiel nannte ich den Satz „Karl ist krank“. In diesem Moment fiel mir siedendheiß
ein, dass ich unbedingt einen lebenden Menschen namens Karl brauchte, auf den
sich der Satz bezog. Andernfalls konnte man den Satz weder als wahr noch als
falsch bezeichnen, d. h. er war gar keine Aussage. Um den Schaden wieder gut
zu machen, fragte ich in den Saal: „Ist jemand unter ihnen, der Karl heißt?“
Sekundenlange Stille. Dann eine Stimme aus dem Hintergrund: „Der ist krank.“

1.A Logische Systeme

Ja, was ist Logik nun wirklich? So genau können wir dies leider auch nicht beschrei-
ben. Das Wort „Logik“ entstammt dem altgriechischen Wort „logos“, welches „Ver-
nunft“ bedeutet. Im allgemeinen Sprachgebrauch bedeutet Logik die Fähigkeit, fol-
gerichtig (also „logisch“) zu denken. In diesem Buch widmen wir uns hauptsächlich
der formalen Logik, also dem Studium der formalen Beziehungen zwischen Denk-
inhalten. Der Prototyp einer mathematischen Beschreibung solcher Denkinhalte ist
der der Aussage, für die wir die folgende Pseudodefinition anzubieten haben.

Definition 1.1
Eine (logische) Aussage ist ein sprachliches Gebilde, das entweder wahr oder falsch
ist.

Wie die obige Anekdote zeigt, hat diese Definition einige Macken, die wir im Rahmen
dieser Einführung aber großzügig übersehen wollen. Die Begriffe wahr und falsch,
die sozusagen vom Himmel fallen und nicht weiter spezifiziert werden, sollen natür-
lich die mit ihnen üblicherweise verbundenen Wahrheitswerte repräsentieren. Statt
wahr schreiben wir oftmals auch 1 und statt falsch verwenden wir meist 0. In einem
gewissen Sinn beschäftigt sich die formale Logik mit „Aussagen über Aussagen“.

Beispiel 1.2
Die folgenden sprachlichen Gebilde stellen Beispiele für Aussagen dar.
A = „Berlin ist die Hauptstadt von Deutschland.“
B = „Der Wal ist ein Fisch.“
C = „Für jede Zahl x ∈ gilt x 2 ≥ 0.“
D = „Das Programm MyProg (…) terminiert.“
Hingegen stellen die folgenden sprachlichen Gebilde „Aussagen über Aussagen“ dar.
E = „Die Aussagen A und B sind beide wahr.“
F = „Die Aussage B gilt nicht.“ = „Der Wal ist kein Fisch.“

14

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 1.A Logische Systeme

Das sprachliche Gebilde „Morgen wird es regnen“ ist jedoch keine Aussage im Sinn
von Definition 1.1, denn ihr Wahrheitswert hängt vom Standpunkt des Betrachters
ab.

In der mathematischen Logik wird eine Symbolisierung der Aussagen vorgenommen.

Anstelle einer Aussage betrachten wir also ein Aussagensymbol (z. B. A oder B). Diese
Aussagensymbole können wir dann mit Junktoren (d. h. Verknüpfungen wie „und
zugleich“ oder „nicht“) zu komplizierteren logischen Formeln zusammensetzen. Je
nachdem, mit welchen Wahrheitswerten die Aussagensymbole belegt werden, er-
halten solche logische Formeln ebenfalls Wahrheitswerte. Die Regeln, nach denen
Aussagensymbole oder allgemeiner so genannte atomare Formeln zu komplizierteren
Formeln zusammengesetzt werden, nennt man die Syntax eines logischen Systems.
Die Regeln, nach denen logische Formeln mit Wahrheitswerten versehen werden,
nennt man die Semantik eines logischen Systems.
Schließlich bleibt noch eine Aufgabe: Wie kann man feststellen, ob eine logische
Formel unter allen möglichen Belegungen der atomaren Formeln mit Wahrheitswerten
stets den Wahrheitswert „wahr“ liefert? Oder ob sie stets den Wahrheitswert „falsch“
liefert? Dies ist die Aufgabe eines logischen Kalküls und obwohl man auch logische
Systeme ohne Kalkül betrachten kann, fehlt diesen doch das Salz in der Suppe. Insge-
samt kann man die im weiteren Verlauf dieses Buches studierten logischen Systeme
also folgendermaßen definieren.

Definition 1.3
Ein logisches System besteht aus den folgenden Teilen.

a) Gewisse formale Ausdrücke werden als atomare Formeln bezeichnet. Die Syntax
des logischen Systems legt fest, wie man die atomaren Formeln mit Hilfe gewisser
Junktoren oder Operatoren zu komplizierteren Formeln zusammenfügen darf.
Die sich ergebenden logischen Formeln sind dabei erst einmal nur nach gewissen
Regeln erstellte Zeichenketten ohne „Inhalt“ oder „Bedeutung“.
b) Die Semantik des logischen Systems besteht aus einer Reihe von Regeln, die fest-
legen, wie die Formeln mit Wahrheitswerten versehen werden können. Dadurch
erhalten die Formeln eine gewisse „Bedeutung“ oder „Interpretation“. Eine Be-
legung der atomaren Formeln mit Wahrheitswerten, für die eine Gesamtformel F
den Wert „wahr“ ergibt, nennt man ein Modell für F. Besitzt F kein Modell, so
heißt F eine unerfüllbare Formel. Liefert F bei jeder Belegung den Wert „wahr“,
so heißt F eine Tautologie oder eine allgemein gültige Formel.
c) Optional gibt es für ein logisches System auch ein logisches Kalkül (oder einfach
Kalkül). Ein Kalkül besteht aus einer Reihe von mechanisch anzuwendenden,
starren Regeln für die Umformung von Formeln. Das Ziel der Anwendung eines
logischen Kalküls ist es, die Unerfüllbarkeit einer vorgegebenen Formel nachzu-
weisen oder ein Modell für sie zu konstruieren. Kalküle eignen sich meist für die
algorithmische Implementierung im Computer.

Das einfachste logische System ist die Aussagenlogik, die im nächsten Abschnitt
ausführlich untersucht werden wird. Hier wollen wir nur die vorstehende Definition
an ihrem Beispiel mit etwas Leben erfüllen.

15

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 1 WAS IST LOGIK?

Beispiel 1.4: Die Aussagenlogik als logisches System

In der Aussagenlogik verknüpfen wir Aussagensymbole A, B, C, … mit Junktoren

∧ „logisches und“
∨ „logisches oder“
¬ „Negation“

So ist z. B. F = (A ∧ ¬B) ∨ (A ∧ C) eine syntaktisch korrekte Formel. Um dieser Formel

einen Wahrheitswert zuzuordnen, betrachten wir z. B. die Belegung

α : {A, B, C} → {0, 1}
A → 1
B → 0
C → 0 .

Unter dieser Belegung gilt dann α (A) = 1, α (¬B) = 1 und daher α (A ∧ ¬B) = 1.
Ferner gilt α (A) = 1, α (C) = 0, also α (A ∧ C) = 0. Schließlich ergibt sich α (F) = 1.
Somit ist α ein Modell für F.

Für die Aussagenlogik gibt es mehrere Kalküle. Bestandteil solcher Kalküle sind meist
Regeln für Äquivalenzumformungen von Formeln. Dies bedeutet, dass man Formeln
in andere Formeln überführt, die bei jeder Belegung denselben Wahrheitswert liefern
und deswegen für die Untersuchung der Unerfüllbarkeit bzw. Allgemeingültigkeit als
zu der Ausgangsformel gleichwertig betrachtet werden können.
Auf den ersten Blick mag es überraschen, dass man bei einem logischen Kalkül
i. A. nur die Unerfüllbarkeit einer Formel bzw. einer Formelmenge nachzuweisen
sucht. Jedoch ist eine Formel F genau dann allgemein gültig, wenn ihre Negation ¬F
unerfüllbar ist. Ebenso ist eine Formel G genau dann eine Folgerung aus einer Menge
von Formeln {F1 , …, Fn }, wenn die Formel F1 ∧ · · · ∧ Fn ∧ ¬G unerfüllbar ist. Alle drei
Aufgaben sind also äquivalent.

1.B Anwendungen
Nun heißt dieses Buch aber nicht „Logik“ oder „Mathematische Logik“, sondern „Lo-
gik für Informatiker“. Was also hat die Logik mit der Informatik zu tun? Ist sie in
der Informatik zu irgend etwas anderem gut, als Studenten zu piesacken? Und wel-
che andere Antwort als „Ja“ kann es auf eine solche rhetorische Frage schon geben?
Nachfolgend listen wir einige Anwendungen der Logik auf, die für die Informatiker
nützlich bzw. interessant sind, und setzen sie in Verbindung zu den später vorgestell-
ten logischen Systemen.
I Lösung einfacher logischer Zusammenhänge („Logeleien“, logische Knobelaufga-
ben), vgl. Kapitel 2.
I Logik-Programmierung (PROLOG), vgl. Abschnitt 3.C.
I Automatische Computerbeweise, vgl. Beispiel 4.64.
I Auffinden und Beweis neuer Gesetzmäßigkeiten oder Formeln in durch Gleichun-
gen beschriebenen Situationen, vgl. Kapitel 5.

16

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 1.B Anwendungen

I Realisation komplizierter Datenstrukturen und Funktionen aus einfachen Baustei-

nen (z. B. Stacks und Stackoperationen), vgl. Beispiel 5.35.
I Beschreibung logischer Bedingungen, die vom Zeitpunkt oder äußeren Bedingun-
gen (z. B. Programmzustand, Variablenwerte) abhängen; Verifikation von Program-
men, die von solchen Bedingungen abhängen, vgl. Kapitel 6.
I Spezifikation und Verifikation paralleler Programme und zeitabhängiger Programm-
abläufe mit Hilfe der Zeitlogik und der Temporallogik, vgl. Kapitel 7.
I Beschreibung des Ein- und Ausgabeverhaltens von Programmen mit Hilfe der dy-
namischen Logik, vgl. Abschnitt 8.A.
I Modellierung von while-Schleifen und if -Abfragen in der Logik PDL, vgl. Ab-
schnitt 8.A.
I Untersuchung des Abbruchverhaltens von Programmen, Verifikation andauernd
laufender Programme mit Hilfe der Prozesslogik, vgl. Abschnitt 8.B.
I Modellierung von Kenntnisständen und Erwartungen in der AI, Analyse von Daten-
bank-Management-Systemen mit Hilfe der intuitionistischen Logik, vgl. Ab-
schnitt 8.C.
I Automatische Erzeugung von Algorithmen zur Realisierung vorgegebener bere-
chenbarer Funktionen, vgl. Abschnitt 8.C.
I Konstruktion neuer logischer Systeme für gegebene Anwendungen, axiomatische
Beschreibung, Beweis der Vollständigkeit und Korrektheit in Bezug auf die beab-
sichtigte Semantik, vgl. Kapitel 9.
Für alle diejenigen, die sich von keinem dieser Themen angesprochen fühlen, haben
wir schließlich noch eine weitere Anwendung dieses Buches anzubieten: Wir haben
versucht, generös überall lustige Zitate, humorvolle Einleitungen, augenzwinkernde
Beispiele und coole Übungsaufgaben zu verstreuen. Wen dieses Buch nicht ein ein-
ziges Mal zum Schmunzeln oder Lachen bringt, den müssen wir zu unserem größten
Bedauern auf eines der in der Literaturliste aufgeführten Werke verweisen. Zusam-
men mit allen anderen stürzen wir uns jetzt in medias res und tischen unser erstes
logisches System auf: die Aussagenlogik.

In the end,
everything is a gag.
(Charlie Chaplin)

17

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 Aussagenlogik

2.A Grundlagen . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2
2.B Das Resolutionskalkül der Aussagenlogik . . 31

Übungsaufgaben . . . . . . . . . . . . . . . . . . . . . . . . . . 36

ÜBERBLICK

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 2 AUSSAGENLOGIK

Logik ist …
ein netter Gegensatz
zur wirklichen Welt.

Die Aussagenlogik beschäftigt sich, wer hätte das gedacht, mit logischen For-
meln, die aus Aussagen zusammengebaut sind. Aussagen sind dabei sprachliche
Gebilde à la „Karl ist krank“. Damit wir nicht so viel zu schreiben haben, reprä-
sentieren wir sie üblicherweise durch Aussagensymbole, z. B. durch A. Wenn das
nicht ausreicht, können wir auch auf B, C, … oder (falls wir mehr als 26 Aussa-
gen betrachten) auf A1 , A2 , … ausweichen. Was wollen wir mit diesen Aussagen-
symbolen nun anfangen? Wir können sie negieren (Schreibweise ¬A) oder mit
den Junktoren „oder“ bzw. „und“ zu komplizierteren Formeln zusammenfügen
(Schreibweise A ∨ B bzw. A ∧ B). Und dann? Dann basteln wir Formeln, deren
Wahrheitswert komplizierte zusammengesetzte Aussagen widerspiegelt, z. B. das
folgende Gespräch dreier Politiker nach einer Bundestagswahl, bei der keine der
Parteien eine klare Mehrheit erreichen konnte:

Angela: „Franz oder ich werden an der Regierungskoalition beteiligt sein.“

Franz: „Entweder Joschka oder ich werden an der Regierung beteiligt sein.“
Joschka: „Entweder Angela oder ich werden in der Opposition sein.“

Aussagenlogisch betrachtet entsprechen diese Behauptungen der Formel

G = (A ∨ F) ∧ ((F ∧ ¬J) ∨ (¬F ∧ J)) ∧ ((A ∧ ¬J) ∨ (¬A ∧ J))

und schon durch Ausprobieren aller Möglichkeiten (weiter unten als „Wahr-
heitstafelmethode“ bezeichnet) finden wir heraus, dass die Politiker uns die Re-
gierungskoalition verraten haben. Offensichtlich wird diese Ausprobiermethode
desto weniger durchführbar, je mehr Aussagensymbole in einer Formel vorkom-
men.
Gibt es einen systematischen Weg, die möglichen Wahrheitswerte einer For-
mel zu bestimmen? Ja, und der Hauptteil dieses Abschnitts dient dazu, das Re-
solutionskalkül der Aussagenlogik vorzustellen. Aber schön langsam, eins nach
dem anderen: Zuerst einmal legen wir den Grundstein und im Gegensatz zur
wirklichen Welt läuft alles ganz klar und einfach ab. Los geht’s!

2.A Grundlagen
Nicht aller Anfang ist schwer. Unser Exkurs in die mathematische Logik beginnt mit
der Syntax der Aussagenlogik und diese ist leicht verdaulich.

Definition 2.1: Die Syntax der Aussagenlogik

a) Eine atomare Formel ist von der Form Ai mit i ∈ N, d. h. atomare Formeln sind
nur die einfachen Aussagen.
b) Eine beliebige Formel entsteht induktiv aus atomaren Formeln, wobei die folgen-
den Schritte erlaubt sind:

20

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 2.A Grundlagen

b1) Jede atomare Formel ist eine Formel.

b2) Sind F, G zwei Formeln, so sind auch (F ∧ G) sowie (F ∨ G) Formeln.
b3) Für jede Formel F ist auch ¬F eine Formel.

Hierbei heißt
F ∧G die Konjunktion von F und G,
F ∨G die Disjunktion von F und G, und
¬F die Negation von F.

Nun betrachten wir einige Beispiele aussagenlogischer Formeln.

Beispiel 2.2
Seien A1 , A2 , A3 Aussagen.
a) Der Ausdruck (¬A1 ∨ (A2 ∧ ¬A3 )) ist eine Formel.
b) Auch ((A1 ∧ A2 ) ∨ A3 ) ist eine Formel, aber
c) A1 ∧ A2 ∨ A3 ist keine Formel, denn die Klammerung fehlt. (Die Junktoren ∧ und
∨ binden gleich stark.)

Zur Vereinfachung der Konstruktion von Formeln führen wir die folgenden Abkür-
zungen ein.

Notationen 2.3
a) Für Aussagen verwenden wir statt A0 , A1 , A2 , … auch A, B, C etc.
Seien nun Formeln F1 , F2 , F3 , … gegeben.
b) Für (¬F1 ∨ F2 ) schreiben wir auch (F1 ⇒ F2 ). Wir nennen F1 ⇒ F2 eine Folgerung.
c) Für (F1 ∧ F2 ) ∨ (¬F1 ∧ ¬F2 ) schreiben wir auch (F1 ⇔ F2 ). Wir nennen F1 ⇔ F2
eine Äquivalenz.

n
d) Für (· · · ((F1 ∨ F2 ) ∨ F3 ) ∨ · · · ∨ Fn ) schreiben wir auch Fi .
i=1

n
e) Für (· · · ((F1 ∧ F2 ) ∧ F3 ) ∧ · · · ∧ Fn ) schreiben wir auch Fi .
i=1

Als Nächstes wollen wir die konstruierten Formeln mit Bedeutungsinhalten versehen.
Anders ausgedrückt, wir wollen die Semantik der Aussagenlogik definieren.

Definition 2.4: Die Semantik der Aussagenlogik

a) Die Elemente der Menge {wahr, falsch} heißen die Wahrheitswerte. Wir schreiben
auch 1 statt wahr und 0 statt falsch.
b) Sei M eine Menge von atomaren Formeln. Eine Belegung von M ist eine Abbildung
α : M → {0, 1}.
c) Sei M die Menge aller Formeln, die mit Hilfe der atomaren Formeln in M gebildet
werden können, und sei α : M → {0, 1} eine Belegung. Dann erweitern wir α zu
einer Abbildung 
α: M → {0, 1} gemäß den folgenden Vorschriften.

21

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 2 AUSSAGENLOGIK

c1) Für atomare Formeln A ∈ M gilt α (A) = α (A).

 gilt
c2) Für Formeln F, G ∈ M

1 falls 
α (F) = 1 und 
α (G) = 1 ,

α ((F ∧ G)) =
0 sonst .

 gilt
c3) Für Formeln F, G ∈ M

1 falls 
α (F) = 1 oder 
α (G) = 1 (oder beides) ,

α ((F ∨ G)) =
0 sonst .

 gilt  1 falls 
α (F) = 0 ,
c4) Für F ∈ M α (¬F) =
0 sonst .
Im Folgenden schreiben wir der Einfachheit halber α statt 
α. Ist eine Belegung der
in einer Formel vorkommenden Aussagensymbole gegeben, so ist der Wahrheits-
wert der Formel gemäß dieser Definition leicht zu ermitteln.

Beispiel 2.5
Seien A, B, C Aussagen und sei α : {A, B, C} → {0, 1} mit α (A) = 1, α (B) = 1 und
α (C) = 0 eine Belegung. Dann gilt:

1 falls α (A) = α (B ∨ ¬C) = 1 ,
α ((A ∧ (B ∨ ¬C))) =
0 sonst ,

1 falls α (B) = 1 oder α (¬C) = 1 (denn α (A) = 1) ,
=
0 sonst ,
= 1 (da z. B. α (B) = 1 gilt) .

Wie können wir einen Überblick über alle möglichen Wahrheitswerte einer Formel
erhalten? Wenn die Formel nicht zu kompliziert ist, funktioniert die folgende Wahr-
heitstafelmethode.

Bemerkung 2.6: Wahrheitstafeln

Seien F, G zwei Formeln und α : M → {0, 1} eine Belegung der in F und G vorkom-
menden atomaren Formeln.
a) Die Wirkung von ∧ ist gegeben durch die Wahrheitstafel:

α (F) α (G) α (F ∧ G)
0 0 0
0 1 0
1 0 0
1 1 1

Dies entspricht dem sprachlichen Gebrauch von „und“ im Sinne von „sowohl als
auch“.

22

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 2.A Grundlagen

b) Die Wirkung von ∨ ist gegeben durch die Wahrheitstafel:

α (F) α (G) α (F ∨ G)
0 0 0
0 1 1
1 0 1
1 1 1

Dies entspricht dem sprachlichen Gebrauch von „oder“ im nicht exklusiven Sinne.
c) Die Wirkung von ¬ ist gegeben durch die Wahrheitstafel:

α (F) α (¬F)
0 1
1 0

Dies entspricht dem sprachlichen Gebrauch von „nicht“.

d) Die Wirkung von ⇒ ist gegeben durch die Wahrheitstafel:

α (F) α (G) α (F ⇒ G)
0 0 1
0 1 1
1 0 0
1 1 1

Dies entspricht dem sprachlichen Gebrauch von „wenn F gilt, dann gilt G“. Dies
wird manchmal auch ausgedrückt in der Form „F gilt nur, falls G gilt“.
e) Die Wirkung von ⇔ ist gegeben durch die Wahrheitstafel:

α (F) α (G) α (F ⇔ G)
0 0 1
0 1 0
1 0 0
1 1 1

Dies entspricht dem sprachlichen Gebrauch von „F gilt genau dann, wenn G gilt“.

Es ist klar, dass man auch für kompliziertere aussagenlogische Formeln mit Hilfe von
Wahrheitstafeln den Wahrheitswert unter jeder denkbaren Belegung ermitteln kann
(vgl. auch Beispiel 2.9). Allerdings werden diese Wahrheitstafeln sehr schnell zu groß
und unübersichtlich.

23

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET

 2 AUSSAGENLOGIK

Beispiel 2.7: Philosophisches

Platon hatte Recht mit seiner Einschätzung des Sokrates genau dann, wenn So-
krates kein großer Philosoph war. Wenn Sokrates ein großer Philosoph war, dann
hatte Aristoteles Recht mit seiner Einschätzung des Platon. Aristoteles hatte nur
dann Recht mit seiner Einschätzung des Platon, falls Platon Recht hatte mit seiner
Einschätzung des Sokrates.

Übersetzen Sie den Text in eine aussagenlogische Formel.

1) Festlegung der Abkürzungen:

S = „Sokrates war ein großer Philosoph.“

A = „Aristoteles hat Recht mit seiner Einschätzung des Platon.“
P = „Platon hatte Recht mit seiner Einschätzung des Sokrates.“

2) Übersetzung der Aussagen:

– „Platon hatte Recht mit seiner Einschätzung des Sokrates genau dann,
wenn Sokrates kein großer Philosoph war.“
2.6.e)
F1 := (P ⇔ ¬S)
– „Wenn Sokrates ein großer Philosoph war, dann hatte Aristoteles Recht
mit seiner Einschätzung des Platon.“
2.3.b)
F2 := (S ⇒ A) = (¬S ∨ A)
– „Aristoteles hatte nur dann Recht mit seiner Einschätzung des Platon,
falls Platon Recht hatte mit seiner Einschätzung des Sokrates.“
2.3.b)
F3 := (A ⇒ P) = (¬A ∨ P)
– Alle Aussagen zusammen werden beschrieben durch die Formel
F := (F1 ∧ F2 ) ∧ F3 .

Definition 2.8
Sei F eine aussagenlogische Formel und sei α : M → {0, 1} eine Belegung.

a) Sind alle in F vorkommenden atomaren Formeln in M enthalten, so heißt α zu F

passend.
b) Ist α zu F passend und gilt α (F) = 1, so schreiben wir α |= F. Wir sagen, dass F
unter der Belegung α gilt und nennen α ein Modell für F.
c) Ist F eine Menge aussagenlogischer Formeln, so heißt α ein Modell für F , wenn
für alle F ∈ F gilt: α |= F. In diesem Fall schreiben wir α |= F .
d) Eine Menge F von Formeln heißt erfüllbar, falls F mindestens ein Modell besitzt.
Ansonsten heißt F unerfüllbar.
e) Eine Formel F heißt allgemein gültig oder eine Tautologie, wenn jede zu F pas-
sende Belegung ein Modell für F ist.

24

Pearson/7215 Kreuzer/Kühling — Logik für Informatiker November 3, 2011 10:15 CET