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 |α|)
Semantik der Aussagenlogik Definition 5 (Bewertung, Interpretation)
Bemerkungen:
Semantik der Aussagenlogik Definition 6 (Bewertung aussagenlogischer Formeln)
Semantik der Aussagenlogik Definition 6 (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 7 (Koinzidenztheorem)
Bemerkungen:
Semantik der Aussagenlogik Definition 8 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 8 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 8 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 8 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 8 (Wahrheitstafel)
Semantik der Aussagenlogik Definition 9 (Erfüllbarkeitsbegriffe)
Semantik der Aussagenlogik Definition 9 (Erfüllbarkeitsbegriffe)
Semantik der Aussagenlogik Definition 9 (Erfüllbarkeitsbegriffe)
Semantik der Aussagenlogik Definition 9 (Erfüllbarkeitsbegriffe)
Bemerkungen:
Semantik der Aussagenlogik Satz 10 (Erfüllbarkeitsbegriffe)
Semantik der Aussagenlogik Definition 11 (Semantische Folgerung)
Semantik der Aussagenlogik Definition 11 (Semantische Folgerung)
Semantik der Aussagenlogik Definition 11 (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:
Eigenschaften des Folgerungsbegriffs Lemma 12 (über aussagenlogische Formeln α und β)
Eigenschaften des Folgerungsbegriffs Lemma 13 (Deduktionstheorem)
Bemerkungen:
Eigenschaften des Folgerungsbegriffs Beweis (Deduktionstheorem)
Eigenschaften des Folgerungsbegriffs Korollar 14 (Deduktionstheorem für endliches M )
Bemerkungen:
Äquivalenz Problematik:
Äquivalenz Definition 16 (logische Äquivalenz)
Äquivalenz Lemma 17
Äquivalenz Wichtige Äquivalenzen zur Formeltransformation\u002f-vereinfachung
Äquivalenz Wichtige Äquivalenzen zur Formeltransformation\u002f-vereinfachung
Äquivalenz Definition 18 (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
Normalformen Erste Stufe einer Normalisierung:
Normalformen Erste Stufe einer Normalisierung:
Normalformen Definition 19 (Negationsnormalform)
Normalformen Algorithmus: NNF
Normalformen Definition 21 (Literal)
Normalformen Definition 23 (Konjunktive Normalform)
Normalformen Lemma 24 (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 25 (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 28 (disjunktive Normalform)
Bemerkungen:
Normalformen Definition 30 (duale Formel)
Normalformen Lemma 31 (duale Formeln und Erfüllbarkeit)
Normalformen Definition 32 (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
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:
Semantische Bäume Definition 33 (1-Äquivalenzen, 0-Äquivalenzen)
Semantische Bäume Definition 34 (1-Reduktion, 0-Reduktion)
Semantische Bäume α
Semantische Bäume Beschränkung der Formelstruktur: Sei α ∈ KNF, A ∈ atoms(α)
Weiterentwicklung semantischer Bäume Verbesserung von SPLIT-SAT.
Weiterentwicklung semantischer Bäume Verallgemeinerung von α[A\u002f1].
Weiterentwicklung semantischer Bäume Davis-Putnam-Algorithmus
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 36 (Schlussregel, Kalkül)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Definition 37 (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-136
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 39 (Resolutionskalkül)
Syntaktische Schlussfolgerungsverfahren Definition 39 (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 40 (Syntax und Semantik im Resolutionskalkül)
Syntaktische Schlussfolgerungsverfahren Satz 40 (Syntax und Semantik im Resolutionskalkül)
Syntaktische Schlussfolgerungsverfahren Satz 40 (Syntax und Semantik im Resolutionskalkül)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Beweis (Skizze)
Bemerkungen:
Syntaktische Schlussfolgerungsverfahren Satz 41 (Laufzeit des Resolutionskalküls)
Syntaktische Schlussfolgerungsverfahren Satz 41 (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 50 (SAT∗)
Erfüllbarkeitsprobleme Definition 52 (SAT)
Erfüllbarkeitsprobleme Definition 54 (3SAT)
Erfüllbarkeitsprobleme Wiederholung (theoretische Informatik)
Erfüllbarkeitsprobleme Definition 57 (DEDUCT)
Erfüllbarkeitsprobleme Definition 59 (EQUIV)
Erfüllbarkeitsprobleme Definition 61 (2SAT)
Erfüllbarkeitsprobleme Beweis (Skizze: Komplexität von 2SAT)
Erfüllbarkeitsprobleme Definition 63 (SAT-Probleme in HORN)
Erfüllbarkeitsprobleme
Kapitel L:III III. Prädikatenlogik
Prädikatenlogik Modell, Formalisierung und natürliche Sprache.
Prädikatenlogik Beispiel „Graphentheorie“.
Prädikatenlogik Beispiel „Graphentheorie“ – Formalisierung der Frage.
Prädikatenlogik Beispiel „Graphentheorie“ – alternative Axiomatisierung.
Prädikatenlogik Beispiel „Blocks World“.
Prädikatenlogik Beispiel „Blocks World“.
Prädikatenlogik Charakteristika der Prädikatenlogik erster Stufe:
Bemerkungen:
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:
Semantik der Prädikatenlogik Definition 7 (Interpretation)
Bemerkungen:
Semantik der Prädikatenlogik Beispiel.
Semantik der Prädikatenlogik Definition 7 (Interpretation – Fortsetzung)
Bemerkungen:
Semantik der Prädikatenlogik Definition 7 (Interpretation – Fortsetzung)
Semantik der Prädikatenlogik Lemma 8 (Koinzidenztheorem)
Semantik der Prädikatenlogik Beispiel.
Semantik der Prädikatenlogik Analog zur Aussagenlogik seien folgende Begriffe definiert:
Semantik der Prädikatenlogik Lemma 9
Wichtige Äquivalenzen Lemma 11
Wichtige Äquivalenzen Vererbung
Wichtige Äquivalenzen (Fortsetzung) Quantorwechsel
Wichtige Äquivalenzen Folgende Äquivalenzen gelten nicht:
Kapitel L:III III. Prädikatenlogik
Einfache Normalformen Definition 8 (Negationsnormalform)
Einfache Normalformen Definition 10 (pränexe Normalform)
Einfache Normalformen Erzeugung einer pränexen Normalform.
Einfache Normalformen Lemma 11
Substitution Beobachtung.
Substitution Definition 12 (Substitution)
Substitution Definition 12 (Substitution)
Bemerkungen:
Substitution Definition 13 (Substitution mit Ersetzungsliste)
Bemerkungen:
Substitution Lemma 14
Bemerkungen:
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 15 (Skolemisierung)
Skolem-Normalformen Definition 17 (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 22 (Herbrand-Interpretation)
Standard-Erfüllbarkeit Satz 23
Standard-Erfüllbarkeit Sei α eine geschlossene Formel in Skolem-Normalform und I eine
Bemerkungen:
Standard-Erfüllbarkeit Beispiel.
Standard-Erfüllbarkeit Satz 26 (Endlichkeitssatz)
Bemerkungen:
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 29 (Unifikationsverfahren nach Robinson)
Bemerkungen:
Prädikatenlogische Resolution Mengenorientierte Schreibweise der Resolutionsregel:
Prädikatenlogische Resolution Satz 31
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 32
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 (Fuzzy Sets) 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:
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:
Modifizierer für Fuzzy-Mengen Beispiel
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
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
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
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
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
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 16 (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 17 (Hoare-Regel)
Verifikation mit dem Hoare-Kalkül Definition 18 (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