Logik-basierte Wissensrepräsentation für mathematisch/technisches Wissen - Cheatsheet

Aussagenlogik und Prädikatenlogik

Definition:

Aussagenlogik und Prädikatenlogik bilden die Grundlage der logikbasierten Wissensrepräsentation. Sie ermöglichen die formale Darstellung und Manipulation von Wissen durch mathematische Logik.

Details:

• Aussagenlogik (AL): Arithmetik von Wahrheitswerten. Bestandteile: Aussagen, Operatoren (AND \( \land \), OR \( \lor \), NOT \( eg \)). Kein interner Strukturbezug.
• Syntax: \( p, q, r, ... \) = Aussagen; \( p \land q, eg r, ... \) = zusammengesetzte Aussagen.
• Semantik: Wahrheitstabelle zur Bewertung von Aussagen
• Prädikatenlogik (PL): Erweiterung der AL. Bestandteile: Variablen, Quantoren (ALLE \( \forall \), EIN \( \exists \)), Prädikate. Interner Strukturbezug.
• Syntax: \( P(x), Q(x,y), ... \) = Prädikate; \( \forall x P(x) \rightarrow Q(x) \), \( \exists y (R(y) \land S(y)) \) = zusammengesetzte Ausdrücke.
• Semantik: Interpretation durch eine Struktur (Domäne + Zuweisung).

Syntax und Semantik von logischen Systemen

Definition:

Syntax beschreibt die formalen Regeln zur Bildung gültiger Ausdrücke, Semantik bezieht sich auf die Bedeutung dieser Ausdrücke.

Details:

• Syntax: strikte Regeln für die Konstruktion von Formeln; beinhaltet Symbole, Operatoren und die Strukturierung von Ausdrücken.
• Semantik: legt fest, wie die Zeichenketten interpretiert werden; Bewertung von Ausdrücken als wahr oder falsch in einem Modell.
• Logische Systeme: Kombination aus Syntax und Semantik; ermöglicht präzise Wissensrepräsentation und logisches Schließen.
• Formale Sprache: definiert durch ein Alphabet und Grammatiken zur Bildung von wohldefinierten Formeln.
• Interpretation: Zuordnung von Wahrheitswerten zu Aussagen auf Basis eines Modells \((\mathcal{M})\).
• Beispiel: In Prädikatenlogik Syntax geregelt durch Variablen, Konstanten, Junktoren, Quantoren; Semantik durch Interpretation der Variablen in Domänen.

Normalformen und Resolution

Definition:

Umformungen logischer Formeln in eine standardisierte Form, um die Anwendung von Resolution zu erleichtern.

Details:

• Konjunktive Normalform (KNF): Eine Formel in KNF ist eine Konjunktion von Disjunktionen von Literalen.
• Disjunktive Normalform (DNF): Eine Formel in DNF ist eine Disjunktion von Konjunktionen von Literalen.
• Resolution: Ein Verfahren zum Beweis der Unerfüllbarkeit, basiert auf der Ableitung eines leeren Klausels durch Resolutionsregeln.
• Algorithmus:
• 1. Formel in KNF umwandeln
• 2. Unit-Resolution und Subsumption anwenden
• 3. Resolutionsregel immer weiter anwenden bis keine neuen Klauseln mehr abgeleitet werden können

Ontologien und Taxonomien

Definition:

Ontologien: formale Darstellung von Wissen mittels Konzepten und Relationen. Taxonomien: hierarchische Klassifikationsschemata.

Details:

• Ontologien: Konzepte, Relationen, Axiome zur Repräsentation von Wissen.
• Formalisierungen: Beschreibung mittels logischer Ausdrücke.
• Taxonomien: Baumstruktur zur Kategorisierung von Wissen.
• Beispiele: Klassifikation von Lebewesen, Verzeichnisstrukturen in Betriebssystemen.
• Wichtig für: Wissensmanagement, Datenintegration, Maschinelles Lernen.
• Verwendung von Ontologien: Unterstützung bei der Beantwortung komplexer Anfragen.
• Verwendung von Taxonomien: Einfache Navigation und Suche von Informationen.

Einführung in Logikprogrammierung

Definition:

Einführung in die Verwendung logischer Regeln zur Programmierung und Wissensrepräsentation.

Details:

• Verwendung von Logiken (meist Prädikatenlogik) zur Programmierung
• Fokus auf was wahr ist und nicht wie es berechnet wird
• Hauptsprache ist Prolog
• Fakten, Regeln und Abfragen sind die grundlegenden Bausteine
• Unifikation und Backtracking sind wichtige Mechanismen
• Mathematische/logische Probleme effizient lösen

Prolog und andere logikbasierte Programmiersprachen

Definition:

Prolog ist eine logikbasierte Programmiersprache, die vor allem für Wissensrepräsentation und künstliche Intelligenz verwendet wird.

Details:

• Prolog (Programmierung in Logik) nutzt Prädikatenlogik erster Stufe.
• Grundelemente: Fakten, Regeln und Abfragen.
• Backtracking und Unifikation sind zentrale Mechanismen.
• Wichtige Syntaxelemente: Klauseln, Prädikate und Variablen.
• Beispiel: \texttt{mensch(sokrates). sterblich(X) :- mensch(X).}
• Andere logikbasierte Sprachen: Datalog, Answer Set Programming (ASP).

Sat-Solver und Modellprüfung

Definition:

SAT-Solver und Modellprüfung sind Verfahren zur automatischen Überprüfung logischer Formeln und Modelle auf Erfüllbarkeit.

Details:

• SAT-Solver: Ansatz zur Lösung von Erfüllbarkeitsproblemen (SAT).
• Modellprüfung (Model Checking): Verifikation von Modellen gegen spezifizierte Eigenschaften.
• SAT: Ermittlung, ob eine Formel in konjunktiver Normalform (CNF) erfüllbar ist.
• Model Checking: Einsatz in der Verifikation von Hardware und Software.
• Nutzung von Algorithmen wie DPLL und CDCL in SAT-Solvern.
• Eigenschaften wie Sicherheit und Korrektheit im Model Checking überprüft.

Formale Spezifikationssprachen

Definition:

Formale Sprachen zur präzisen Beschreibung von Softwaresystemen und deren Verhalten.

Details:

• Verwendung: Spezifikation und Verifikation von Software
• Mathematische Grundlage: Logik und Mengenlehre
• Typen: Z, VDM, B, Alloy
• Ziele: Fehlerreduktion, Dokumentation, Automatisierung