Logik Theo Lettmann
Inhalt I. Einführung
Ziele Wie können aus vorhandenem Wissen Schlussfolgerungen gezogen werden?
Angrenzende Gebiete 1. Formale Sprachen
Literatur
Kapitel L:II II. Aussagenlogik
Syntax der Aussagenlogik Definition 1 (Sprache der Aussagenlogik)
Bemerkungen:
Syntax der Aussagenlogik Vereinbarungen:
Syntax der Aussagenlogik Definition 3 (atoms(α))
Syntax der Aussagenlogik
Bemerkungen:
Syntax der Aussagenlogik Definition 4 (Formellänge |α|)
Syntax der Aussagenlogik Definition 4 (Formellänge |α|)
Kapitel L:II II. Aussagenlogik
Semantik der Aussagenlogik Definition 5 (Bewertung, Interpretation)
Bemerkungen:
Semantik der Aussagenlogik Definition 6 (Bewertung aussagenlogischer Formeln)
Semantik der Aussagenlogik Definition 7 (Bewertung aussagenlogischer Formeln
Bemerkungen:
Semantik der Aussagenlogik Die Formalisierung von Aussagen über die Realität mittels der Sprache der
Semantik der Aussagenlogik Die Formalisierung von Aussagen über die Realität mittels der Sprache der
Semantik der Aussagenlogik Die Formalisierung von Aussagen über die Realität mittels der Sprache der
Semantik der Aussagenlogik Die Formalisierung von Aussagen über die Realität mittels der Sprache der
Semantik der Aussagenlogik Die Formalisierung von Aussagen über die Realität mittels der Sprache der
Semantik der Aussagenlogik Satz 8 (Koinzidenztheorem)
Bemerkungen:
Semantik der Aussagenlogik Definition 9 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 9 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 9 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 9 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 9 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 10 (Erfüllbarkeitsbegriffe)
Semantik der Aussagenlogik Definition 10 (Erfüllbarkeitsbegriffe)
Semantik der Aussagenlogik Definition 10 (Erfüllbarkeitsbegriffe)
Semantik der Aussagenlogik Definition 10 (Erfüllbarkeitsbegriffe)
Bemerkungen:
Semantik der Aussagenlogik Satz 11 (Erfüllbarkeitsbegriffe)
Semantik der Aussagenlogik Definition 12 (Semantische Folgerung)
Semantik der Aussagenlogik Definition 12 (Semantische Folgerung)
Semantik der Aussagenlogik Definition 12 (Semantische Folgerung)
Semantik der Aussagenlogik Zeichen der Objektsprache
Semantik der Aussagenlogik Zeichen der Metasprache
Semantik der Aussagenlogik Zeichen der Metasprache
Bemerkungen:
Semantik der Aussagenlogik Beispiele für Formeln aus Aussagenlogik und Algebra:
Semantik der Aussagenlogik Beispiele für Formeln aus Aussagenlogik und Algebra:
Semantik der Aussagenlogik Beispiele für Formeln aus Aussagenlogik und Algebra:
Semantik der Aussagenlogik Weitere Vereinbarungen zur Syntax:
Bemerkungen:
Kapitel L:II II. Aussagenlogik
Eigenschaften des Folgerungsbegriffs Lemma 13 (über aussagenlogische Formeln α und β)
Eigenschaften des Folgerungsbegriffs Lemma 14 (Deduktionstheorem)
Bemerkungen:
Eigenschaften des Folgerungsbegriffs Beweis (Deduktionstheorem)
Eigenschaften des Folgerungsbegriffs Korollar 15 (Deduktionstheorem für endliches M )
Bemerkungen:
Kapitel L:II II. Aussagenlogik
Äquivalenz Problematik:
Äquivalenz Definition 17 (logische Äquivalenz)
Äquivalenz Lemma 18
Äquivalenz Wichtige Äquivalenzen zur Formeltransformation/-vereinfachung
Äquivalenz Wichtige Äquivalenzen zur Formeltransformation/-vereinfachung
Äquivalenz Definition 19 (Erfüllbarkeitsäquivalenz)
Äquivalenz Veranschaulichung der Formeln hinsichtlich ihrer Erfüllbarkeit:
Bemerkungen:
Kapitel L:II II. Aussagenlogik
Formeltransformation Jede Formel kann als Datenstruktur in der Form eines Baumes interpretiert werden:
Formeltransformation Die Ersetzung eines Vorkommens von γ in α durch δ entspricht der Ersetzung eines
Formeltransformation Aus Sicht der maschinellen Verarbeitung hätte man gerne kanonische Formeln
Formeltransformation Aus Sicht der maschinellen Verarbeitung hätte man gerne kanonische Formeln
Kapitel L:II II. Aussagenlogik
Normalformen Erste Stufe einer Normalisierung:
Normalformen Erste Stufe einer Normalisierung:
Normalformen Definition 20 (Negationsnormalform)
Normalformen Algorithmus: NNF
Normalformen Definition 22 (Literal)
Normalformen Definition 24 (Konjunktive Normalform)
Normalformen Lemma 25 (logisch äquivalente KNF)
Normalformen Algorithmus:
Normalformen Beispiel zum exponentiellen Platzbedarf.
Normalformen Beispiel zum exponentiellen Platzbedarf.
Normalformen Beispiel zum exponentiellen Platzbedarf.
Formeltransformation nach Tseitin Andere Idee zur Erzeugung einer KNF aus α:
Formeltransformation nach Tseitin ∧
Formeltransformation nach Tseitin ∧
Formeltransformation nach Tseitin ∧
Formeltransformation nach Tseitin ∧
Bemerkungen:
Formeltransformation nach Tseitin Lemma 26 (erfüllbarkeitsäquivalente KNF)
Bemerkungen:
Normalformen Frage: Gegeben eine Formel ∈ KNF. Inwieweit lassen sich die Klausellängen unter
Normalformen Frage: Gegeben eine Formel ∈ KNF. Inwieweit lassen sich die Klausellängen unter
Bemerkungen:
Normalformen Definition 29 (disjunktive Normalform)
Bemerkungen:
Normalformen Definition 31 (duale Formel)
Normalformen Lemma 32 (duale Formeln und Erfüllbarkeit)
Normalformen Definition 33 (Mengenschreibweise für Formeln in KNF)
Bemerkungen:
Kapitel L:II II. Aussagenlogik
Bedeutung der Folgerung Q. Warum ist der Begriff der Folgerung so wichtig?
Bedeutung der Folgerung Q. Warum ist der Begriff der Folgerung so wichtig?
Bedeutung der Folgerung Q. Warum ist der Begriff der Folgerung so wichtig?
Bedeutung der Folgerung Q. Wenn Folgern lediglich Explizitmachen ist, warum hat dann das Überprüfen oder Erzeugen
Bedeutung der Folgerung Q. Wenn Folgern lediglich Explizitmachen ist, warum hat dann das Überprüfen oder Erzeugen
Kapitel L:II II. Aussagenlogik
Erfüllbarkeitsalgorithmen Q. Was hat die Beantwortung der Folgerungsfrage „Gilt α |= β ?“ mit dem Erfüllbarkeitsproblem
Erfüllbarkeitsalgorithmen Verschiedene Möglichkeiten, die Erfüllbarkeit einer Formel α zu entscheiden.
Erfüllbarkeitsalgorithmen Verschiedene Möglichkeiten, die Erfüllbarkeit einer Formel α zu entscheiden.
Erfüllbarkeitsalgorithmen Semantische Bäume
Bemerkungen:
Kapitel L:II II. Aussagenlogik
Semantische Bäume Definition 34 (1-Äquivalenzen, 0-Äquivalenzen)
Semantische Bäume Definition 35 (1-Reduktion, 0-Reduktion)
Semantische Bäume α
Semantische Bäume Beschränkung der Formelstruktur: Sei α ∈ KNF, A ∈ atoms(α)
Kapitel L:II II. Aussagenlogik
Weiterentwicklung semantischer Bäume Verbesserung von SPLIT-SAT.
Weiterentwicklung semantischer Bäume Verallgemeinerung von α[A/1].
Weiterentwicklung semantischer Bäume Davis-Putnam-Algorithmus [Davis/Putnam 1960, Davis/Loveland/Logemann 1962]
Weiterentwicklung semantischer Bäume Beispiel für DPLL-SAT:
Weiterentwicklung semantischer Bäume Auswahlkriterien für Splittingregel:
Weiterentwicklung semantischer Bäume Auswahlkriterien für Splittingregel:
Weiterentwicklung semantischer Bäume Auswahlkriterien für Splittingregel:
Kapitel L:II II. Aussagenlogik
Syntaktische Schlussfolgerungsverfahren Ausgangspunkt ist die Frage: „Gilt α |= β ?“
Syntaktische Schlussfolgerungsverfahren Definition 37 (Schlussregel, Kalkül)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Definition 38 (Herleiten, syntaktisches Schlussfolgern)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Die Schlussregel Modus Ponens, MP (drei Schreibweisen)
Syntaktische Schlussfolgerungsverfahren Die Schlussregel Modus Ponens, MP (drei Schreibweisen)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Eigenschaften von Kalkülen
Syntaktische Schlussfolgerungsverfahren Eigenschaften von Kalkülen
Syntaktische Schlussfolgerungsverfahren Eigenschaften von Kalkülen
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Korrektheit der Schlussregel MP
Syntaktische Schlussfolgerungsverfahren Vollständigkeit des MP
Syntaktische Schlussfolgerungsverfahren Vollständigkeit des MP
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Beispiel: Herleitung von β aus α = γ ∧ (¬γ ∨ β).
Syntaktische Schlussfolgerungsverfahren Beispiel: Herleitung von β aus α = γ ∧ (¬γ ∨ β).
Syntaktische Schlussfolgerungsverfahren Beispiel: Herleitung von β aus α = γ ∧ (¬γ ∨ β).
Syntaktische Schlussfolgerungsverfahren Beispiel: Herleitung von β aus α = γ ∧ (¬γ ∨ β).
Syntaktische Schlussfolgerungsverfahren Weitere Schlussregeln sind denkbar – z. B. der Kettenschluss, KS:
L:II-143
Syntaktische Schlussfolgerungsverfahren Die Schlussregel Resolution (Formeln in KNF, Mengenschreibweise)
Syntaktische Schlussfolgerungsverfahren Die Schlussregel Resolution (Formeln in KNF, Mengenschreibweise)
Syntaktische Schlussfolgerungsverfahren Die Schlussregel Resolution
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Definition 40 (Resolutionskalkül)
Syntaktische Schlussfolgerungsverfahren Definition 40 (Resolutionskalkül)
Syntaktische Schlussfolgerungsverfahren Beispiel (Input-Resolution).
Syntaktische Schlussfolgerungsverfahren Beispiel.
Syntaktische Schlussfolgerungsverfahren Beispiel (reguläre Resolution).
Syntaktische Schlussfolgerungsverfahren Beispiel (reguläre Resolution).
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Beispiel (lineare Resolution immer möglich).
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Beispiel.
Syntaktische Schlussfolgerungsverfahren Satz 41 (Syntax und Semantik im Resolutionskalkül)
Syntaktische Schlussfolgerungsverfahren Satz 41 (Syntax und Semantik im Resolutionskalkül)
Syntaktische Schlussfolgerungsverfahren Satz 41 (Syntax und Semantik im Resolutionskalkül)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Beweis (Skizze)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Satz 42 (Laufzeit des Resolutionskalküls)
Syntaktische Schlussfolgerungsverfahren Satz 42 (Laufzeit des Resolutionskalküls)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Die Varianten des Resolutionskalküls können als verschiedene Strategien
Syntaktische Schlussfolgerungsverfahren zu 1. Varianten in der Struktur des Herleitungsbaums
Syntaktische Schlussfolgerungsverfahren zu 2. Varianten semantischer Konzepte
Syntaktische Schlussfolgerungsverfahren zu 2. Varianten semantischer Konzepte
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren zu 2. Varianten semantischer Konzepte
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Wichtige Resultate für Resolutionskalküle
Syntaktische Schlussfolgerungsverfahren Wichtige Resultate für Resolutionskalküle
Syntaktische Schlussfolgerungsverfahren Zusammenfassung
Kapitel L:II II. Aussagenlogik
Erfüllbarkeitsprobleme Wiederholung (theoretische Informatik)
Erfüllbarkeitsprobleme Wiederholung (theoretische Informatik)
Erfüllbarkeitsprobleme Wiederholung (theoretische Informatik)
Bemerkungen:
Erfüllbarkeitsprobleme Wiederholung (theoretische Informatik)
Bemerkungen:
Erfüllbarkeitsprobleme Wiederholung (theoretische Informatik)
Erfüllbarkeitsprobleme Definition 51 (SAT∗)
Erfüllbarkeitsprobleme Definition 53 (SAT)
Erfüllbarkeitsprobleme Definition 55 (3SAT)
Erfüllbarkeitsprobleme Wiederholung (theoretische Informatik)
Erfüllbarkeitsprobleme Definition 58 (DEDUCT)
Erfüllbarkeitsprobleme Definition 60 (EQUIV)
Erfüllbarkeitsprobleme Definition 62 (2SAT)
Erfüllbarkeitsprobleme Beweis (Skizze: Komplexität von 2SAT)
Erfüllbarkeitsprobleme Definition 64 (SAT-Probleme in HORN)
Erfüllbarkeitsprobleme
Kapitel L:III III. Prädikatenlogik
Motivation Modell, Formalisierung und natürliche Sprache.
Motivation Beispiel „Graphentheorie“.
Motivation Beispiel „Graphentheorie“ – Formalisierung der Frage.
Motivation Beispiel „Graphentheorie“ – alternative Axiomatisierung.
Motivation Beispiel „Blocks World“.
Motivation Beispiel „Blocks World“.
Motivation Charakteristika der Prädikatenlogik erster Stufe:
Bemerkungen:
Kapitel L:III III. Prädikatenlogik
Syntax der Prädikatenlogik Definition 1 (Sprache der Prädikatenlogik, Signatur)
Syntax der Prädikatenlogik Definition 2 (Terme)
Syntax der Prädikatenlogik Definition 3 (prädikatenlogische Formeln)
Bemerkungen:
Syntax der Prädikatenlogik Beispiele.
Syntax der Prädikatenlogik Beispiel „Stetigkeit in x0“.
Syntax der Prädikatenlogik Beispiel „Stetigkeit in x0“.
Syntax der Prädikatenlogik Bindungsstärke:
Syntax der Prädikatenlogik
Syntax der Prädikatenlogik Definition 4 (enthaltene Variablen)
Syntax der Prädikatenlogik Definition 5 (gebundene und freie Variablen)
Syntax der Prädikatenlogik Definition 6 (geschlossene Formel)
Bemerkungen: Ob es sich bei einer Variable um eine freie oder eine gebundene Variable handelt, muss für
Kapitel L:III III. Prädikatenlogik
Semantik der Prädikatenlogik Definition 7 (Interpretation)
Bemerkungen: Im folgenden wird auch xU abkürzend für I(x), aU für I(a), fU für I(f (n) ) und PU für
Semantik der Prädikatenlogik Beispiel.
Semantik der Prädikatenlogik Definition 8 (Interpretation – Fortsetzung)
Bemerkungen:
Semantik der Prädikatenlogik Definition 9 (Interpretation – Fortsetzung)
Semantik der Prädikatenlogik Lemma 10 (Koinzidenztheorem)
Semantik der Prädikatenlogik Beispiel.
Semantik der Prädikatenlogik Analog zur Aussagenlogik seien folgende Begriffe definiert:
Semantik der Prädikatenlogik Lemma 11
Kapitel L:III III. Prädikatenlogik
Wichtige Äquivalenzen Lemma 13
Wichtige Äquivalenzen Vererbung
Wichtige Äquivalenzen (Fortsetzung) Quantorwechsel
Wichtige Äquivalenzen Folgende Äquivalenzen gelten nicht:
Kapitel L:III III. Prädikatenlogik
Einfache Normalformen Definition 14 (Negationsnormalform)
Einfache Normalformen Definition 16 (pränexe Normalform)
Einfache Normalformen Erzeugung einer pränexen Normalform.
Einfache Normalformen Lemma 17
Kapitel L:III III. Prädikatenlogik
Substitution Beobachtung.
Substitution Definition 18 (Substitution)
Substitution Definition 18 (Substitution)
Bemerkungen:
Substitution Definition 19 (Substitution mit Ersetzungsliste)
Bemerkungen:
Substitution Lemma 20
Bemerkungen:
Kapitel L:III III. Prädikatenlogik
Skolem-Normalformen Eigenschaften freier Variablen:
Skolem-Normalformen Modellierung basiert auf:
Skolem-Normalformen Existenzquantoren werden in jeder Interpretation so gedeutet, dass in Abhängigkeit
Skolem-Normalformen Definition 21 (Skolemisierung)
Skolem-Normalformen Definition 23 (Skolem-Normalform)
Bemerkungen:
Skolem-Normalformen Zusammenfassung: Vorgehensweise zur Umwandlung nach SKNF.
Bemerkungen:
Skolem-Normalformen Wiederholung: ∀x (α ∧ β) ≈ ∀x α ∧ ∀xβ
Skolem-Normalformen Analog zur Aussagenlogik können lassen sich weitere Einschränkungen an die
Kapitel L:III III. Prädikatenlogik
Standard-Erfüllbarkeit Problem.
Bemerkungen:
Standard-Erfüllbarkeit Beispiele.
Standard-Erfüllbarkeit Und wie weiter?
Standard-Erfüllbarkeit Definition 28 (Herbrand-Interpretation)
Standard-Erfüllbarkeit Satz 29
Standard-Erfüllbarkeit Sei α eine geschlossene Formel in Skolem-Normalform und I eine
Bemerkungen:
Standard-Erfüllbarkeit Beispiel.
Standard-Erfüllbarkeit Satz 32 (Endlichkeitssatz)
Bemerkungen:
Kapitel L:III III. Prädikatenlogik
Prädikatenlogische Resolution Beobachtung.
Prädikatenlogische Resolution Motivation.
Bemerkungen:
Prädikatenlogische Resolution Aussagenlogische Resolution:
Bemerkungen:
Prädikatenlogische Resolution Ziel bei der Unifikation: So wenig spezialisieren, wie möglich.
Bemerkungen:
Prädikatenlogische Resolution Wie bestimmt man den allgemeinsten Unifikators für zwei Primformeln P (t1, . . . , tn)
Bemerkungen:
Prädikatenlogische Resolution Definition 35 (Unifikationsverfahren nach Robinson)
Bemerkungen:
Prädikatenlogische Resolution Mengenorientierte Schreibweise der Resolutionsregel:
Prädikatenlogische Resolution Satz 37
Prädikatenlogische Resolution Sei α eine Formel in Klauselnormalform. Verfahren zur Generierung einer
Bemerkungen:
Kapitel L:III III. Prädikatenlogik
Grenzen der Prädikatenlogik Dadurch, dass wir bisher keine Möglichkeit vorgesehen haben, in den Formeln die
Bemerkungen:
Grenzen der Prädikatenlogik Durch die Gleichheit hat man nun die Möglichkeit, bestimmte Anzahlen von
Grenzen der Prädikatenlogik Die Formel
Grenzen der Prädikatenlogik Satz 38
Kapitel L:IV IV. Nichtklassische Logiken
Fuzzy-Mengen Unscharfes Wissen
Fuzzy-Mengen Unscharfes Wissen
Fuzzy-Mengen Unscharfes Wissen
Bemerkungen:
Fuzzy-Mengen Unscharfes Schlussfolgern
Fuzzy-Mengen Unscharfes Schlussfolgern
Fuzzy-Mengen Geschichte
Fuzzy-Mengen Die traditionelle Mengenlehre malt ein Schwarz-Weiß-Bild von der Welt: ein Objekt
Fuzzy-Mengen Beispiel Alter (
Fuzzy-Mengen Definition 1 (Fuzzy-Menge, Zugehörigkeitsfunktion)
Fuzzy-Mengen Definition 1 (Fuzzy-Menge, Zugehörigkeitsfunktion)
Bemerkungen:
Fuzzy-Mengen Beispiel: Raumtemperatur
Fuzzy-Mengen Konstruktion
Fuzzy-Mengen Konstruktion
Fuzzy-Mengen Konstruktion
Fuzzy-Mengen Schreibweise
Fuzzy-Mengen Schreibweise
Fuzzy-Mengen Charakterisierung
Fuzzy-Mengen Charakterisierung
Bemerkungen:
Kapitel L:IV IV. Nichtklassische Logiken
Modifizierer für Fuzzy-Mengen Im täglichen Sprachgebrauch spielen Adverbien bei der Beschreibung von
Modifizierer für Fuzzy-Mengen Beispiel:
Modifizierer für Fuzzy-Mengen Definition 3 (Modifizierer für Fuzzy-Menge)
Modifizierer für Fuzzy-Mengen Beispiel:
Dann gilt: Asehralt =
Modifizierer für Fuzzy-Mengen Beispiel
Kapitel L:IV IV. Nichtklassische Logiken
Operationen auf Fuzzy-Mengen Klassische Mengen A ⊂ X:
Operationen auf Fuzzy-Mengen Definition 4 (Mengenoperationen auf Fuzzy-Mengen)
Bemerkungen:
Operationen auf Fuzzy-Mengen Definition 4
Operationen auf Fuzzy-Mengen Definition 4
Operationen auf Fuzzy-Mengen Definition 4
Bemerkungen:
Operationen auf Fuzzy-Mengen Beispiel:
Operationen auf Fuzzy-Mengen Für ∪, ∩ und ¬ und für beliebige Fuzzy-Mengen A, B und C über einem
Operationen auf Fuzzy-Mengen Beweis des Satzes von de Morgan für Fuzzy-Mengen:
Operationen auf Fuzzy-Mengen Konstruktion neuer Fuzzy-Mengen
Operationen auf Fuzzy-Mengen t-Normen
Operationen auf Fuzzy-Mengen t-Normen
Operationen auf Fuzzy-Mengen t-Normen
Operationen auf Fuzzy-Mengen t-Normen
Operationen auf Fuzzy-Mengen t-Normen
Operationen auf Fuzzy-Mengen t-Normen
Kapitel L:IV IV. Nichtklassische Logiken
Fuzzy-Inferenz Aussagenlogik versus Fuzzy-Logik
Bemerkungen:
Fuzzy-Inferenz Generalisierter Modus Ponens
Fuzzy-Inferenz Generalisierter Modus Ponens
Fuzzy-Inferenz Generalisierter Modus Ponens
Fuzzy-Inferenz Generalisierter Modus Ponens
Fuzzy-Inferenz Generalisierter Modus Ponens
Fuzzy-Inferenz Max-Min-Inferenz[Mamdani 1977]
Fuzzy-Inferenz Vektor-Matrix-Multiplikation
Fuzzy-Inferenz Vektor-Matrix-Multiplikation
Fuzzy-Inferenz Vektor-Matrix-Multiplikation
Fuzzy-Inferenz Max-Min-Inferenz
Fuzzy-Inferenz Max-Min-Inferenz
Fuzzy-Inferenz Max-Min-Inferenz
Fuzzy-Inferenz Max-Min-Inferenz
Fuzzy-Inferenz Max-Min-Inferenz
Fuzzy-Inferenz Max-Min-Inferenz
Bemerkungen:
Fuzzy-Inferenz Max-Produkt-Inferenz
Fuzzy-Inferenz Max-Produkt-Inferenz
Bemerkungen:
Fuzzy-Inferenz Regeln mit mehreren Prämissen
Fuzzy-Inferenz Multiple Regeln
Bemerkungen:
Fuzzy-Inferenz Multiple Regeln
Fuzzy-Inferenz Multiple Regeln
Kapitel L:IV IV. Nichtklassische Logiken
Defuzzifizierung Defuzzifizierung ist die Generierung scharfer Werte einer induzierten Fuzzy-Menge
Bemerkungen:
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Produktionsregelsysteme Vergleich von Deduktions- und Produktionsregelsystem
Produktionsregelsysteme Vergleich von Deduktions- und Produktionsregelsystem
Produktionsregelsysteme Definition 1 (Produktionsregelsystem)
Bemerkungen:
Produktionsregelsysteme Definition 2 (Semantik Produktionsregelsystem)
Produktionsregelsysteme Definition 3 (Ableitung)
Bemerkungen:
Produktionsregelsysteme Regelinterpreter
Produktionsregelsysteme Regelinterpreter
Produktionsregelsysteme Definition 4 (kommutativ)
Produktionsregelsysteme Definition 4 (kommutativ)
Produktionsregelsysteme Realisierung des Interpreters durch Regelverkettung
Produktionsregelsysteme Realisierung des Interpreters durch Regelverkettung
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Inferenz für Produktionsregelsysteme Vorwärtsverkettende Verfahren (Forward-Chaining)
Inferenz für Produktionsregelsysteme Vorwärtsverkettende Verfahren (Forward-Chaining)
Inferenz für Produktionsregelsysteme Recognize-Act-Zyklus realisiert als Forward-Chaining
Inferenz für Produktionsregelsysteme Eigenschaften des Algorithmus FC
Inferenz für Produktionsregelsysteme Ableitbarkeitstest durch Forward-Chaining
Bemerkungen:
Inferenz für Produktionsregelsysteme Recognize-Act-Zyklus realisiert als Backward-Chaining
Inferenz für Produktionsregelsysteme Definition 7 (Und-Oder-Baum)
Inferenz für Produktionsregelsysteme Beispiel: Und-Oder-Baum
Inferenz für Produktionsregelsysteme Algorithmus für das Backward-Chaining
Inferenz für Produktionsregelsysteme Algorithmus für das Backward-Chaining
Inferenz für Produktionsregelsysteme Bedingungen ohne Disjunktion
Inferenz für Produktionsregelsysteme Bedingungen ohne Disjunktion
Inferenz für Produktionsregelsysteme Definition 8 (Ableitungsbaum)
Inferenz für Produktionsregelsysteme Beispiel: Ableitungsbaum für Backward-Chaining
Inferenz für Produktionsregelsysteme Analyse von Backward-Chaining mit Regelgraphen
Inferenz für Produktionsregelsysteme Analyse von Backward-Chaining mit Regelgraphen
Inferenz für Produktionsregelsysteme Beispiel: Regelgraph
Bemerkungen:
Inferenz für Produktionsregelsysteme Beispiel: Zyklische Regelmenge
Inferenz für Produktionsregelsysteme Laufzeit für Backward-Chaining
Inferenz für Produktionsregelsysteme Beweis Laufzeit BC-DFS
Inferenz für Produktionsregelsysteme Verkettungsstrategien
Inferenz für Produktionsregelsysteme Verkettungsstrategien
Inferenz für Produktionsregelsysteme Verkettungsstrategien
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Produktionsregelsysteme mit Negation Definition 12 (PS mit Negation)
Produktionsregelsysteme mit Negation Vereinfachung von Bedingungsteilen mit NOT
Produktionsregelsysteme mit Negation Vereinfachung von Bedingungsteilen mit NOT
Produktionsregelsysteme mit Negation Interpretation von NOT als Negation-as-Failure
Produktionsregelsysteme mit Negation Interpretation von NOT als Negation-as-Failure
Bemerkungen:
Produktionsregelsysteme mit Negation Algorithm:
Produktionsregelsysteme mit Negation Algorithm:
Produktionsregelsysteme mit Negation Zyklische Regelmengen und NOT
Produktionsregelsysteme mit Negation Negation-as-Failure und Vorwärtsverkettung
Produktionsregelsysteme mit Negation Negation-as-Failure und Vorwärtsverkettung
Produktionsregelsysteme mit Negation Interpretation von NOT bzgl. statischer Datenbasis und Vorwärtsverkettung
Produktionsregelsysteme mit Negation Lemma 15
Produktionsregelsysteme mit Negation Algorithm:
Bemerkungen:
Produktionsregelsysteme mit Negation Satz 16 (Korrektheit und Vollständigkeit von FC-N-test)
Produktionsregelsysteme mit Negation Beweis (Korrektheit und Vollständigkeit von FC-N-test)
Produktionsregelsysteme mit Negation Nicht-Determinismus von FC-N-test
Produktionsregelsysteme mit Negation Beweis (Skizze: NP-Vollständigkeit des Ableitbarkeitsproblems)
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Nicht-monotones Schließen Problemlösen mittels Logik
Bemerkungen:
Nicht-monotones Schließen Schlussfolgern in der klassischen Logik
Nicht-monotones Schließen Schlussfolgern in der klassischen Logik
Nicht-monotones Schließen Schlussfolgern in der klassischen Logik
Bemerkungen:
Nicht-monotones Schließen Schlussfolgern über Nicht-Wissen: Negation-as-Failure
Bemerkungen:
Nicht-monotones Schließen Schlussfolgern über Nicht-Wissen: Default-Logik [Doyle/McDermott 1980]
Bemerkungen:
Nicht-monotones Schließen Schlussfolgern über Nicht-Wissen
Bemerkungen:
Nicht-monotones Schließen Schlussfolgern über Nicht-Wissen
Nicht-monotones Schließen Schlussfolgern über Nicht-Wissen
Bemerkungen:
Nicht-monotones Schließen Operationalisierung
Nicht-monotones Schließen Operationalisierung
Bemerkungen:
Nicht-monotones Schließen Modellierung
Bemerkungen:
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Logik und abstrakte Algebren Logik
Logik und abstrakte Algebren Interpretation
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Bemerkungen:
Verifikation Software-Qualität
Verifikation Software-Qualität
Verifikation Software-Qualität
Verifikation Anwendungsbedarf
Verifikation Anwendungsbedarf
Verifikation Testen als Alternative
Verifikation Testen als Alternative
Verifikation Aufgaben bei der Softwareentwicklung
Verifikation Korrektheitsprüfung: Softwaretest
Verifikation Algorithmus und Programm
Verifikation Algorithmus und Programm
Verifikation Arten von Programmierparadigmen
Verifikation Programmierparadigmen
Verifikation Programmierparadigmen
Verifikation Eine einfache imperative Programmiersprache
Verifikation Eine einfache imperative Programmiersprache
Verifikation Eine einfache imperative Programmiersprache
Verifikation Eine einfache imperative Programmiersprache
Bemerkungen:
Verifikation Beispiel für ein Programm
Verifikation Einfache imperative Programmiersprache
Verifikation Beispiel für ein Programm
Verifikation Semantik formaler Sprachen
Verifikation Semantik formaler Sprachen
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Verifikation mit dem Hoare-Kalkül Der Hoare-Kalkül (auch Hoare-Logik) ist ein Formales System,
Verifikation mit dem Hoare-Kalkül Imperative Programmierung
Verifikation mit dem Hoare-Kalkül Annotation durch Zusicherungen
Verifikation mit dem Hoare-Kalkül Spezifikation als spezielle Zusicherungen
Verifikation mit dem Hoare-Kalkül Beispiel für eine Spezifikation
Verifikation mit dem Hoare-Kalkül Verifikation auf Basis von Zusicherungen
Verifikation mit dem Hoare-Kalkül Verifikation auf Basis von Zusicherungen
Verifikation mit dem Hoare-Kalkül Verifikation auf Basis von Zusicherungen
Verifikation mit dem Hoare-Kalkül Verifikation auf Basis von Zusicherungen
Verifikation mit dem Hoare-Kalkül Definition 18 (Hoare-Formel)
Verifikation mit dem Hoare-Kalkül Verifikation auf Basis axiomatischer Semantik
Verifikation mit dem Hoare-Kalkül Verifikation auf Basis axiomatischer Semantik
Verifikation mit dem Hoare-Kalkül Beispiel für ein Programm
Verifikation mit dem Hoare-Kalkül Definition 19 (Hoare-Regel)
Verifikation mit dem Hoare-Kalkül Definition 20 (Hoare-Kalkül)
Verifikation mit dem Hoare-Kalkül Kalkül für die einfache imperative Programmiersprache
Verifikation mit dem Hoare-Kalkül Verifikation
Verifikation mit dem Hoare-Kalkül Beipiel einer Verifikation: Addition zweier natürlicher Zahlen
Verifikation mit dem Hoare-Kalkül Beipiel einer Verifikation: Addition zweier natürlicher Zahlen
Verifikation mit dem Hoare-Kalkül Herleitung im Hoare-Kalkül als Baum
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Hoare-Regeln und partielle Korrektheit Hoare-Regel für Zuweisungen
Hoare-Regeln und partielle Korrektheit Beispiele für die Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Abschwächungsregeln
Hoare-Regeln und partielle Korrektheit Beispiele für die Anwendung der Abschwächungsregeln
Hoare-Regeln und partielle Korrektheit Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Zuweisungsregel
Hoare-Regeln und partielle Korrektheit Hoare-Regeln für Anweisungsfolgen
Hoare-Regeln und partielle Korrektheit Vorgehen bei der Verifikation eines Programmes
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation eines Programmes
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation eines Programmes
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation eines Programmes
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation eines Programmes
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation eines Programmes
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation eines Programmes
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation eines Programmes
Bemerkungen:
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation eines Programmes
Bemerkungen zum Lesen der Tabelle:
Hoare-Regeln und partielle Korrektheit Hoare-Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiele zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Verifikation von bedingten Anweisungen
Hoare-Regeln und partielle Korrektheit Hoare-Regel für Schleifen
Bemerkungen:
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel
Hoare-Regeln und partielle Korrektheit Anwendung der Regeln für bedingte Anweisungen
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel: Abrollen der Schleife
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel: Abrollen der Schleife
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel: Abrollen der Schleife
Hoare-Regeln und partielle Korrektheit Beispiel zur Anwendung der Schleifenregel: Abrollen der Schleife
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel zu Schleifeninvarianten
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Einfaches Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Hoare-Regeln und partielle Korrektheit Beispiel Effizientes Potenzieren
Bemerkungen:
Hoare-Regeln und partielle Korrektheit Möglichkeiten zum Einsparen von Schreibarbeit
Kapitel L:V V. Erweiterungen und Anwendungen zur Logik
Terminierung Der Nachweis der totalen Korrekheit eines Programms erfordert neben der bisher
Bemerkungen:
Terminierung Terminierung von Schleifen
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Bemerkungen:
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Terminierung Formaler Nachweis der Terminierung von Schleifen
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Terminierung Beispiel für den Nachweis der Terminierung einer Schleife
Terminierung Informeller Nachweis der Terminierung von Schleifen
Bemerkungen:
Terminierung Beispiel für den alternativen Nachweis der Terminierung einer Schleife
Terminierung Beispiel für den alternativen Nachweis der Terminierung einer Schleife
Bemerkungen:
Terminierung Terminierung: Ein Problem?
Terminierung Terminierung: Ein Problem?
Terminierung Terminierung: Ein Problem?
Bemerkungen:
Terminierung Nicht-Terminierung von Schleifen
Bemerkungen:
Terminierung Beispiel Nicht-Terminierung von Schleifen
Terminierung Beispiel Nicht-Terminierung von Schleifen
Terminierung Beispiel Nicht-Terminierung von Schleifen
Terminierung Beispiel Nicht-Terminierung von Schleifen
Terminierung Beispiel Nicht-Terminierung von Schleifen
Terminierung Beispiel Nicht-Terminierung von Schleifen