Semantic in Bullets - Logic in detail
- Logik, die Lehre des formalen Schließens
- Semantik
- Syntax → zulässige Zeichenfolgen ohne Bedeutung
- Semantik → Regeln wie Bedeutung komplexer Zeichenfolgen aus der von atomare Zeichenfolgen hergeleitet werden kann
- intendiert
- formal
- prozedural
- Modelltheoretische Semantik: formale Interpretation der Sprache in einem Modell
- Logik besteht aus Menge von Sätzen S und Schlussfolgerungsrelation
- Aussagenlogik
- Negation, Konjunktion, Disjunktion, Implikation, Äquivalenz
- FOL
- Existenz-/Allquantor
- Terme = Variablen, Konstanten- und Funktionssymbole
- Atome = Relationssymbole mit Termen als Argumenten
- Formeln = Atome, Junktoren und Quantoren
- Modeltheoretische Semantik
- Interpretation → abbilden der Atome nach wahr und falsch
- Struktur
- Grundbereich
- Konstanten auf Grundbereich
- Funktionen auf Grundbereich
- Relationen auf Grundbereich
- Zeige dass Formel widerlegbar → nicht allgemeingültig
- logische Konsequenz: jedes Modell von F1 auch modell von F2
- Normalformen
- NegationsNF → Negationen ganz innen
- PränexNF → Quantoren ganz vorne
- gleiche Reihenfolge ggf. umbenennen
- Skolemnisierte PränexNF → Eleminierung der Existenzquantoren
- durch Konstante ersetzen
- bei Allquantor Funktionssymbol
- Konjunktive NF → Konjunktion aus Disjunktionen
- aka Klauselform
- nur noch Allquantoren → weglassen
- Logik rechnen
- Entscheidbarkeit
- Semientscheidbarkeit (Aufzählbarkeit)
- Resolution
- Verfahren
- 1. Wähle Zwei Klausel und erzeuge noch durch Resolutionsschritt
- 2. Ist Klausel immer falsch → Widerspruch
- 3. Sonst, füge Klausel hinzu und gehe zu 1
- Variablenbindung durch Substitution
- Unifikator → nach Substituion Formeln gleich
- endliche Anzahl von Schritten um Widerspruch zu finden
- nicht entscheidbar
- Eigenschaften von FOL Prädikatenlogik
- Monotonie → mit Vergrößerung des Wissens, keine Verlust von Schlussfolgerungen
- Kompaktheit → Schlussfolgerung begründet auf endliche Menge von Sätzen
- nicht entscheidbar
- außer Nachweisen der logischen Konsequenz → semi-entscheidbar
- Eigenschaften der Aussagenlogik
- alles aus FOL
- Schlussfolgerungen sind entscheidbar
