2017-04-18: p 14, Proposition 2.4.2: "und" durch "bzw." ersetzt (6x) p 15, (b), (c), (d): Beweis etwas ausführlicher; abschließender Satz vor 2.5 modifiziert. p 118, Definition A.3.2: Typos: Q bzw. A durch P ersetzt; kleinstes und größtes Element definiert; Komplemente definiert, ebenso die Menge der obenen/unteren Schranken einer Menge. p 118f: neue Definition A.3.3: Halbverbände, (distributive) Verbände, komplementäre Halbordnungen, Boole'sche Algebren 2017-04-19: p 13, Einführender Paragraph von Abschnitt 2.4 leicht modifiziert. p 14, vor Definition 2.4.1: "formalisieren" statt "umsetzen". 2017-04-26: p 116, A.2.2: letzter Punkt: Die Relationen von 1 nach B bzw. umgekehrt werden auch als Funktionen von 1 x B bzw. B x 1 nach 2={0,1} dargestellt, d.h. als binäre 1 x B bzw. B x 1 Matrizen, und weil 1 x B bzw. B x 1 zu B isomorph sind, können diese sog. charakteristischen Funktionen mit den Teilmengen von B identifiziert werden. 2017-04-27: p 117,118: blöde copy-and-paste Fehler in der Definition oberer/unterer Schranken (A.3.2) und bei der Distributivität (A.3.3) behoben. 2017-05-03: p 28, Bemerkung 4.2.4: p 33 und p 37: Kapitel 5 und 6 umgetauscht (betrifft nur die alten Inhaltsverzeichnisse). 2017-05-17: p 40, unten: Korrektur der ersten Resolvente zu {B,-C} 2017-05-21: p 33 Überschrift und andere Stellen: Ersetzung von "semantische Implikation" durch "logische Konsequenz" p 37, 2. Paragraph: Präzisierung, wann die Resolutionsmethode anwendbar ist (bei Prämissen in KNF, es brauchen nicht notwendig Klauseln zu sein, aber man kann KNFs natürlich in Klauseln zerlegen). 2017-05-25: p 53, Abschnitt 7.4: neuer Titel, explizite Definition eines formalen Beweises in Tableaux-Form, leicht überarbeiteter Text. (Dieser Abschnitt war 2017-05-24 noch nicht behandelt worden, um noch weitere Regeln einführen zu können.) 2017-06-25: p 76, 2. Paragraph: Erwähnung charakteristischer Funktionen als bessere Alternative zu Relationen bei der Beschreibung mathematischer Strukturen. Diese ermöglichen auch die Verwendung partieller Funktionen, sollten solche benötigt werden. p 77, 2. Punkt: Präzisierung, dass die Funktionssymbole nicht nur innere Knoten sondern auch Blätter liefern können. p 80, (b): korrigierte Interpretation von R(x,y,z...); es handelt sich um den Wahrheitswert der Behauptung (x,y,z ...) erfülle R, der 0 oder 1 sein kann. 2017-06-26: p 80, 2. Paragraph: verbesserte Beschreibung von Axiomen als Formeln, die immer als wahr interpetiert werden sollen. Dazu gehören insbesondere Gleichungen, also Paare von Termen, die mit \doteq verbunden sind. p 88: Korrigierte Beschreibung des Falles R(x,y); "notationelle" statt "notatinelle" Besipeil 9.4.15: Ergänzung zur Identifikation der Formeln der Aussagenligik mit den Termen für die angegebene Signatur: bis auf die Namen der Variablen Zeile 7 von unten: Punkt über dem Gleichheitszeichen. 2017-06-28: p 86, lange Formel am Ende: fehlendes Klammer-Paar ergänzt (nach \exists\delta) 2017-07-04: p 81+82: Beispiele 9.2.6 und 9.2.7 ergänzt; das war in der VL angespreochen worden. p 84, nach dem oberen Diagramm: Feststellung, dass jede der Mengen T_\Sigma(M) kanonische Interpretationen der Funktionssymbole aus \Sigma zuläßt. p 84, Definition 9.4.4: Text vor der Definition und eigentliche Definition sprachlich und formal bereinigt. p 86, Beispiel 9.4.7: etwas umformuliert, Baum ergänzt (vergl. HA) p 90, Definition 9.5.1: Die Forderung, dass \doteq formal eine Äquvalenzrelation sein soll (reflexiv, transitiv und symmetrisch), wurde ergänzt. p 94, Beispiel 10.0.7 verbessert. 2017-07-10: p 81, Definition 9.2.2: Namen \Sigma_F bzw. \Sigma_P für die Listen der Funktions- und Relationssymbole der Signatur \Sigma eingeführt. p 104, neue Bemerkung 12.0.6: die Pränex-Normalform braucht nicht eindeutig bestimmt zu sein: wenn sie durch Konjunktion oder Disjunktion zweier PNFs entsteht, kann man die beiden Quantorengruppen durchmischen. p 106/107: Satz 12.0.14 und Algorithmus 12.0.15 vorgezogen aus Kapitel 14