Logik  Aussagenlogik

Prädikatenlogik

 
 

Chronologisch

Alphabetisch

Syntax der Prädikatenlogik Variable Prädikatsymbol Funktionssymbol Stellenzahl  Stelligkeit Terme Konstante Prädikatenlogische Formeln Atomare Formeln Sematik der Prädikatenlogik Struktur Grundmenge Universum Wert Wahrheitswert Folgerbarkeit Modell Erfüllbarkeit Ableitbarkeit Generalisierung Substitution -Subsumtion Generalisierte -Subsumtion Generative Klauseln deterministische Klauseln indeterministische Klauseln beschränkte Klauseln constrained k-lokale Hornklauseln k-llokale Hornklauseln k-vlokale Hornklausen Deterministische Tiefe  ij-deterministische Klauseln Logik-Programmierung

Ableitbarkeit Atomare Formeln beschränkte Klauseln constrained Deterministische Klauseln Deterministische Tiefe Erfüll barkeit Folgerbarkeit Funktionssymbol Generalisierte -Subsumtion Generalisierung Generative Klauseln Grundmenge ij-deterministische Klauseln indeterministische Klauseln k-llokale Hornklauseln k-lokale Hornklauseln k-vlokale Hornklausen Konstante Logik-Programmierung Modell Prädikatenlogische Formeln Prädikatsymbol Sematik der Prädikatenlogik Stellenzahl  Stelligkeit Struktur Substitution Syntax der Prädikatenlogik Terme Universum Variable Wahrheitswert Wert -Subsumtion

 

Die Prädikatenlogik ist eine Erweiterung der Aussagenlogik, wobei Quantoren, Funktions- und Prädikatsymbole hinzukommen. Durch diese Konzepte sind Sachverhalte beschreibbar, die im Rahmen der Aussagenlogik nicht formuliert werden können. In der Aussagenlogik war es z.B. nicht möglich auszudrücken, daß gewisse ``Objekte`` in Beziehung stehen; daß eine Eigenschaft für alle Objekte gilt, oder daß ein Objekt mit einer gewissen Eigenschaft existiert.

Syntax der Prädikatenlogik

Eine (prädikatenlogische) Signatur  S ist ein Tupel  , wobei  und  endliche oder abzählbar unendliche Mengen sind mit  und  .

Eine Variable hat die Form  mit  . Ein Prädikatsymbol hat die Form  und ein Funktionssymbol hat die Form  mit  und  . Hierbei heißt i jeweils der Unterscheidungsindex und k die Stellenzahl oder Stelligkeit. Man definiert die Menge der Terme  durch einen induktiven Prozeß:

• Jede Variable ist ein Term.
• Falls f ein Funktionssymbol ist mit Stellenzahl k und falls  Terme sind, so ist auch  ein Term.

Hierbei sollen auch Funktionssymbole der Stellenzahl 0 eingeschlossen sein, und in diesem Fall sollen die Klammern wegfallen. Nullstellige Funktionssymbole heißen auch Konstanten.

Nun kann man die Menge der prädikatenlogischen Formeln  definieren:

• Falls P ein Prädikatsymbol der Stelligkeit k ist, und falls  Terme sind, dann ist  eine Formel.
• Für jede Formel F ist auch  eine Formel.
• Für alle Formeln F und G sind auch  und  Formeln.
• Falls x eine Variable ist und F eine Formel, so sind auch  und  Formeln.

Atomare Formeln nennt man genau die Formeln, die gemäß i) aufgebaut sind. Falls F eine Formel ist und F als Teil einer Formel G auftritt, so heißt F Teilformel von G.

Sematik der Prädikatenlogik

Eine Struktur ist ein Paar , wobei  eine beliebige aber nicht leere Menge ist, die Grundmenge oder Universum von  genannt wird. Ferner ist  eine Abbildung, die

• jedem k-stelligen Prädikatsymbol P (das im Definitionsbereich von  liegt) ein k-stellliges Prädikat über  zuordnet,
• jedem k-stelligen Funktionssymbol f (das im Definitionsbereich von  liegt) eine k-stellige Funktion auf  zuordnet,
• jeder Variablen x (sofern  auf x definiert ist) ein Element der Grundmenge  zuordnet.

Sei F eine Formel und  eine Struktur.  heiát zu F passend, falls  für alle in F vorkommenden Prädikatsymbole, Funktionssymbole und freien Variablen definiert ist.
 
Sei F eine Formel und  eine zu F passende Struktur. Für jeden Term t, den man aus den Bestandteilen von F bilden kann, definiert man den Wert von t in der Struktur  , den man mit  bezeichnet.

i) Falls t eine Variable ist (also t= x), so ist  .
ii) Falls t die Form hat  wobei  Terme und f ein k-stelliges Funktionssymbol ist, so ist

Der Fall ii) schließt auch die Möglichkeit ein, daß f nullstellig ist, also t die Form hat t=a. In diesem Fall ist also  . Auf analoge Weise definiert man den Wahrheitswert der Formeln F unter der Struktur  , wobei man ebenfalls die Bezeichnung  verwendet.

• Falls F die Form hat  mit den Termen  und k-stelligem Prädikatsymbol P, so ist



• Falls F die Form  hat, so ist



• Falls F die Form  hat, so ist



• Falls F die Form  hat, so ist



• Falls F die Form  hat, so ist



• Falls F die Form  hat, so ist

Hierbei ist  diejenige Struktur  , die überall mit  identisch ist, bis auf die Definition von  : Es sei nämlich  , wobei  - unabhängig davon, ob  auf x definiert ist oder nicht.

Die Prädikatenlogik ist in folgendem Sinn eine Erweiterung der Aussagenlogik: Falls alle Prädikatsymbole nullstellig sein müssen erhält man Formeln der Aussagenlogik, wobei die nullstelligen Prädikatsymbole die Rolle der atomaren Formeln der Aussagenlogik übernehmen.

Die Begriffe ``Folgerbarkeit``, ``Modell`` und ``erfüllbar`` lassen sich direkt aus der Aussagenlogik übertragen.

Für die Ableitbarkeit kommen weitere logische Axiome zu denen der Aussagenlogik hinzu. Ausserdem gibt es eine weitere Ableitungsregel, nämlich das Generalisieren.

Substitution

Sei S eine Signatur, s ein Term aus  und x eine Variable.

• ist wie folgt definiert:

Für  entsteht  aus t, indem wir jedes Auftreten von x in t durch s ersetzen.

• Die partielle Abbildung  ist wie folgt definiert:

Für  ist

• ist definiert, falls folgendes der Fall ist:

Wenn wir jedes freie Auftreten von x in A durch s ersetzen, so kommt keine der Variablen in s in den Wirkungsbereich eines Quantors in A.

• Wenn  definiert ist, dann ist  die Formel, die aus A entsteht, wenn wir jedes freie Auftreten von x in A durch s ersetzen.

-Subsumtion

Als Grundlage für die Generalisierungsrelation kann der Forgerungsbegriff verwendet werden. Da die Folgerbarkeit im allgemeinen Fall aber nicht entscheidbar ist, wird die schwächere Subsumtionsbeziehung bevorzugt. Immer, wenn die Subsumtionsbeziehung gilt, gilt auch die logische Folgerung - aber nicht umgekehrt!

Eine Klausel C1 ist genereller als eine andere Klausel C2, wenn gilt: C1 subsumiert C2.

Für Literale gilt:

Ein Literal L1 subsumiert ein anderes Literal L2, wenn es eine Substitution  gibt, so daß  .

Damit wird die Substitution zur Grundlage der Formalisierung der Generalisierung.

Für Hornklauseln gilt folgende Definition der  -Subsumtion:

Eine Hornklausel   -subsumiert eine Hornklausel  , gdw. es eine Substitution  gibt, so daß  , und  .

Generalisierte  -Subsumtion

Die generalisierte  -Subsumtion generalisiert zwei funktionsfreie Hornklauseln bezüglich gegebenem Hintergrundwissen. Die Substitution  führt für alle Variablen der zu generalisierenden Klausel neue Konstante ein.  bezeichne eine Substitution von Termen. Dann ist die Generalisierung nach Buntine folgendermaßen definiert:

Operationalisierung der Definition:

Jede Klausel  der generelleren Klauselmenge kann zurückgeführt werden auf eine Klausel der spezielleren Klauselmenge, indem

• Variablen aus  in Konstante oder andere Terme überführt werden,
• Atome dem Klauselkörper von  hinzugefügt werden, oder
• der Klauselkörper von  im Hinblick auf das Hintergrundwissen B teilweise ausgewertet wird, d.h. ein Atom aus  wird mit einer Klausel aus B resolviert.

Die generalisierte Subsumtion ist nur für eingeschränkte Sprachklassen entscheidbar.

Beschränkungen von Hornklauseln

• Eine Klausel ist generativ, wenn jede Variable aus dem Klauselkopf auch im Klauselkörper vorkommt (  bereichsbeschränkte Klauseln in deduktiven Datenbanken).
• Eine Klausel ist bezüglich B deterministisch, wenn für jedes Literal im Klauselkörper die bereits durch Konstante substituierten Variablen und das Hintergrundwissen eine eindeutige Substitution für die restlichen Variablen des Literals festlegen. Gibt es mehr als eine Sustitution, so ist die Klausel indeterministisch.
• Eine Klausel ist beschränkt (constrained), wenn jede Variable aus dem Klauselkörper auch im Klauselkopf vorkommt.

k-lokale Hornklauseln

Sei D eine Hornklausel,  und vars eine Funktion, die die Menge der Variablen einer Klausel berechnet.  ist ein lokaler Teil von D genau dann, wenn  und es kein  gibt, welches auch ein lokaler Teil von D ist. Ein lokaler Teil  ist für eine Konstante k:
k-vlokaler Teil gdw.  ,
k-llokaler Teil gdw.  .

Eine Hornklausel D heißt k-llokal genau dann, wenn jeder lokale Teil von D ein k-llokaler bzw. ein k-vlokaler Teil ist.

Eine Klausel ist k-lokal, wenn sie einen lokalen Teil von Variablen oder Literalen hat, der k-llokal oder k-vlokal ist.

Deterministische Tiefe eines Terms

Ein Term aus einem Klauselkopf K ist mit einer Kette der Länge 0 verbunden. Für den Klauselkörper nimmt man an, daß die Literale nach ihrer Verbundenheit mit dem Klauselkopf geordnet sind:  . Ein Term t aus  ist genau dann durch eine deterministische Kette der Länge d+1 verbunden, wenn

• alle Terme im Klauselkopf und in  verbunden sind durch deterministische Ketten, die höchstens d lang sind, und
• es für jede Substitution  , die K mit einem Beispiel und die ersten Literale mit dem Hintergrundwissen unifiziert - also  und  - genau eine eindeutige Substitution  gibt, so daá  .

Die minimale Länge der deterministisch verbindenden Ketten ist die determinsistische Tiefe eines Terms.

Eine Klausel ist ij-deterministisch, wenn sie

• deterministisch ist und
• bezüglich B die maximale (deterministische) Tiefe ihrer Terme i ist,

die maximale Stelligkeit ihrer Prädikate j ist.
 

Logik-Programmierung

Das Ausführen eines Programms kann aufgefaßt werden als das (automatische) Herleiten der leeren Klausel aus einer gegebenen Klauselmenge, zusammen mit einer Antworterzeugungskomponente. Die aus dem Resolutionsbeweis extrahierte Antwort kann dann als Rechenergebnis des (Logik-) Programms aufgefaát werden.

Sei eine i.a. erfüllbare Klauselmenge F gegeben. Dieses F kann man als ein (Logik-) Programm auffassen: In F kommen gewisse Prädikate und Funktionen vor und es werden durch die Klauseln in F gewisse Aussagen über deren Beziehung zueinander gemacht.

Es soll durch die Logik-Programmierung nicht nur die Frage, ob die Existenz eines (oder mehrerer) Objekte mit gewissen Eigenschaften aus dem Programm F folgt, vom Auswertungsmechanismus mit ja oder nein beantwortet werden. Es soll vielmehr im ja-Fall ein entsprechendes Objekt (oder möglicherweise alle) ausgegeben werden.

Man will z.B. wissen, ob G aus F folgt. Dazu testet man mittels Resolution, ob  unerfüllbar ist.

  
 Logik  Aussagenlogik
6.2.1998