Hornklausel
Die elementaren Bestandteile von Hornklauseln sind Konstanten und Variablen. Variablen werden durch Symbole dargestellt, deren Name mit einem Großbuchstaben (A-Z) beginnt. Alle anderen Ausdrücke werden als Konstante interpretiert. Aus Konstanten und Variablen werden Terme, Atome, Literale und schließlich Hornklauseln zusammengesetzt.
Ein Term ist entweder eine Konstante oder eine Variable oder eine Struktur. Eine Struktur ist eine Liste, deren erstes Element eine Konstante oder eine Variable ist. Die weiteren Elemente können beliebige Terme sein.
Ein gewöhnliches Atom ist eine Liste, deren erstes Element eine Konstante ist und deren weitere Elemente Terme sind. Ein Atom ist entweder ein gewöhnliches Atom, oder ein Test oder eine Zuweisung. Tests werden durch zweielementige Listen dargestellt, die mit dem Symbol 'true?' beginnen. Die Repräsentation einer Zuweisung ist eine dreielementige Liste mit dem einleitenden Symbol 'is'.
Ein Literal ist entweder ein Atom oder ein negiertes Atom. Negierte Atome werden durch zweielementige Listen mit dem Symbol 'not' am Anfang ausgedrückt.
Für eine Konjunktion von Literalen gibt es drei Fälle: die leere Konjunktion dargestellt durch das Symbol 't', ein einzelnes Literal und eine Liste von mehreren Literalen mit dem vorangestellten Symbol 'and'. Eine Hornklausel ist eine Liste mit drei Elementen: dem Symbol 'implied', einem gewöhnlichen Atom und einer Konjunktion von Literalen. Schließlich besteht ein Programm aus einer Liste von Hornklauseln.
ConstantOrVariable = Constant | Variable.
Term = ConstantOrVariable | '(' ConstantOrVariable {Term} ')'.
OrdinaryAtom = '(' Constant {Term} ')'.
Atom = OrdinaryAtom | '(' 'true?' S-Expression ')' | '(' 'is' ConstantOrVariable S-Expression ')'.
Literal = Atom | '(' 'not' Atom ')'.
LiteralConjunction = 't' | Literal | '(' 'and' {Literal} ')'.
GeneralHornClause = '(' 'implied' OrdinaryAtom LiteralConjunction ')'.
NormalProgram = '(' {GeneralHornClause} ')'.
Mit dem oben beschriebenen Formalismus lässt sich ein (zugegebenermaßen ineffizientes) Sortierprogramm wir folgt darstellen:
(
(implied (sort X Y)
(and
(permutation X Y)
(sorted Y)))
(implied (sorted nil) t)
(implied (sorted (cons X nil)) t)
(implied (sorted (cons X (cons Y YS)))
(and
(true? (less? X Y))
(sorted (cons Y YS))))
(implied (permutation nil nil) t)
(implied (permutation (cons X XS) (cons Y YS))
(and
(delete Y (cons X XS) Z)
(permutation Z YS)))
(implied (delete X (cons X XS) XS) t)
(implied (delete X (cons Y YS) (cons Y Z))
(and
(true? (not (equal? X Y)))
(delete X YS Z)))
)
Angewendet auf das Ziel (sort (cons 4 (cons 1 (cons 3 (cons 2 nil)))) X) ergibt sich X zu (cons 1 (cons 2 (cons 3 (cons 4 nil)))).
Während der Ausführung des Programms wird versucht, dass Ziel zu beweisen. Der Beweisprozess wählt ein Literal des Ziels aus, entfernt es aus dem Ziel und
- fügt die Literale aus dem Rumpf einer Hornklausel in das Ziel ein, wenn das Literal ein gewöhnliches Atom ist, das zum Kopf der Hornklausel passt. Mehrere passende Hornklauseln führen zu einer Verzweigung des Beweisprozesses - die verschiedenen Möglichkeiten werden gleichzeitig verfolgt.
- überprüft, ob der Test zutrifft. Wenn nein, dann ist der Zweig des Beweisprozesses fehlgeschlagen.
- überprüft, ob die Zuweisung ausgeführt werden kann. Wenn nein, dann ist der Zweig des Beweisprozesses fehlgeschlagen.
- startet einen untergeordneten Beweisprozess für das negierte Atom. Wenn der untergeordnete Prozess zum Erfolg führt, dann ist der Zweig des übergeordneten Beweisprozesses fehlgeschlagen.
Ein Zweig eines Beweisprozesses ist erfolgreich, wenn es gelingt, das letzte verbleibende Literal aus dem Ziel zu entfernen.
Zur den Details der Implementierung siehe
- Term,
- Formel,
- Unifikation und
- Resolution.
Das Sortierprogramm oben und weitere Beispiele finden sich in der unten verlinkten Datei. Diese kann mit dem Programm Calc betrachtet werden.
Ein Term ist entweder eine Konstante oder eine Variable oder eine Struktur. Eine Struktur ist eine Liste, deren erstes Element eine Konstante oder eine Variable ist. Die weiteren Elemente können beliebige Terme sein.
Ein gewöhnliches Atom ist eine Liste, deren erstes Element eine Konstante ist und deren weitere Elemente Terme sind. Ein Atom ist entweder ein gewöhnliches Atom, oder ein Test oder eine Zuweisung. Tests werden durch zweielementige Listen dargestellt, die mit dem Symbol 'true?' beginnen. Die Repräsentation einer Zuweisung ist eine dreielementige Liste mit dem einleitenden Symbol 'is'.
Ein Literal ist entweder ein Atom oder ein negiertes Atom. Negierte Atome werden durch zweielementige Listen mit dem Symbol 'not' am Anfang ausgedrückt.
Für eine Konjunktion von Literalen gibt es drei Fälle: die leere Konjunktion dargestellt durch das Symbol 't', ein einzelnes Literal und eine Liste von mehreren Literalen mit dem vorangestellten Symbol 'and'. Eine Hornklausel ist eine Liste mit drei Elementen: dem Symbol 'implied', einem gewöhnlichen Atom und einer Konjunktion von Literalen. Schließlich besteht ein Programm aus einer Liste von Hornklauseln.
ConstantOrVariable = Constant | Variable.
Term = ConstantOrVariable | '(' ConstantOrVariable {Term} ')'.
OrdinaryAtom = '(' Constant {Term} ')'.
Atom = OrdinaryAtom | '(' 'true?' S-Expression ')' | '(' 'is' ConstantOrVariable S-Expression ')'.
Literal = Atom | '(' 'not' Atom ')'.
LiteralConjunction = 't' | Literal | '(' 'and' {Literal} ')'.
GeneralHornClause = '(' 'implied' OrdinaryAtom LiteralConjunction ')'.
NormalProgram = '(' {GeneralHornClause} ')'.
Mit dem oben beschriebenen Formalismus lässt sich ein (zugegebenermaßen ineffizientes) Sortierprogramm wir folgt darstellen:
(
(implied (sort X Y)
(and
(permutation X Y)
(sorted Y)))
(implied (sorted nil) t)
(implied (sorted (cons X nil)) t)
(implied (sorted (cons X (cons Y YS)))
(and
(true? (less? X Y))
(sorted (cons Y YS))))
(implied (permutation nil nil) t)
(implied (permutation (cons X XS) (cons Y YS))
(and
(delete Y (cons X XS) Z)
(permutation Z YS)))
(implied (delete X (cons X XS) XS) t)
(implied (delete X (cons Y YS) (cons Y Z))
(and
(true? (not (equal? X Y)))
(delete X YS Z)))
)
Angewendet auf das Ziel (sort (cons 4 (cons 1 (cons 3 (cons 2 nil)))) X) ergibt sich X zu (cons 1 (cons 2 (cons 3 (cons 4 nil)))).
Während der Ausführung des Programms wird versucht, dass Ziel zu beweisen. Der Beweisprozess wählt ein Literal des Ziels aus, entfernt es aus dem Ziel und
- fügt die Literale aus dem Rumpf einer Hornklausel in das Ziel ein, wenn das Literal ein gewöhnliches Atom ist, das zum Kopf der Hornklausel passt. Mehrere passende Hornklauseln führen zu einer Verzweigung des Beweisprozesses - die verschiedenen Möglichkeiten werden gleichzeitig verfolgt.
- überprüft, ob der Test zutrifft. Wenn nein, dann ist der Zweig des Beweisprozesses fehlgeschlagen.
- überprüft, ob die Zuweisung ausgeführt werden kann. Wenn nein, dann ist der Zweig des Beweisprozesses fehlgeschlagen.
- startet einen untergeordneten Beweisprozess für das negierte Atom. Wenn der untergeordnete Prozess zum Erfolg führt, dann ist der Zweig des übergeordneten Beweisprozesses fehlgeschlagen.
Ein Zweig eines Beweisprozesses ist erfolgreich, wenn es gelingt, das letzte verbleibende Literal aus dem Ziel zu entfernen.
Zur den Details der Implementierung siehe
- Term,
- Formel,
- Unifikation und
- Resolution.
Das Sortierprogramm oben und weitere Beispiele finden sich in der unten verlinkten Datei. Diese kann mit dem Programm Calc betrachtet werden.