Herbrand Universum und Least Herbrand Modell

Question

Ich lese die Frage in Herbrand universe, Herbrand Base and Herbrand Model of binary tree (prolog) und die Antworten gegeben, aber ich habe eine etwas andere Frage mehr wie eine Bestätigung und hoffentlich wird meine Verwirrung geklärt werden.

Sei P ein Programm so beschaffen sein, dass wir die folgenden Tatsachen und haben in der Regel:

q(a, g(b)). 
q(b, g(b)). 
q(X, g(X)) :- q(X, g(g(g(X)))). 

Aus dem obigen Programm, das Herbrand Universum

Up = {a, b, g(a), g(b), q(a, g(a)), q(a, g(b)), q(b, g(a)), q(b, g(b)), g(g(a)), g(g(b))...e.t.c} 

Herbrand Basis:

Bp = {q(s, t) | s, t E Up} 

• Nun komm zu meiner Frage (verzeih Ich für meine Ignoranz), ich habe q (a, g (a)) als ein Element in meinem Herbrand-Universum eingeschlossen, aber aus der Tatsache, es heißt q (a, g (b)). Bedeutet das, dass q (a, g (a)) nicht dort ist?
• Auch, da die Herbrand-Modelle Teil der Herbrand-Basis sind, wie ermittle ich das kleinste Herbrand-Modell durch Induktion?

Anmerkung: Ich habe eine Menge Forschung auf diesem getan, und einige Teile sind mir gut klar, aber ich habe immer noch diesen Zweifel in mir das ist, warum ich die Gemeinden Meinung suchen wollen. Vielen Dank.

Answer 1

Von der Tatsache q(a,g(b)) können Sie nicht schließen, ob q(a,g(a)) in dem Modell ist oder nicht. Sie müssen das Modell zuerst generieren.

Um das Modell zu ermitteln, beginnen Sie mit den Fakten {q(a,g(b)), q(b,g(b))} und versuchen Sie nun, Ihre Regeln anzuwenden, um es zu erweitern. In Ihrem Fall gibt es jedoch keine Möglichkeit, die rechte Seite der Regel q(X,g(X)) :- q(X,g(g(g(X)))). mit den obigen Fakten zu vergleichen. Deshalb bist du fertig.

Jetzt vorstellen die Regel

q(a,g(Y)) :- q(b,Y). 

Diese Regel verwendet werden könnte unser Set zu erweitern. In der Tat, die Instanz

q(a,g(g(b))) :- q(b,g(b)). 

verwendet wird: Wenn q(b,g(b)) vorhanden ist, q(a,g(g(b))) zu schließen. Beachten Sie, dass wir hier die Regel von rechts nach links verwenden. So erhalten wir

{q(a,g(b)), q(b,g(b)), q(a,g(g(b)))} 

damit einen Fixpunkt zu erreichen.

Nun nehmen Sie als weiteres Beispiel die Regel vorgeschlagen

q(X, g(g(g(X)))) :- q(X, g(X)). 

die es erlaubt, (ich werde nicht mehr die instanziiert Regel zeigen) in einem Schritt zu erzeugen:

{q(a,g(b)), q(b,g(b)), q(a,g(g(g(b)))), q(b, g(g(g(b))))} 

Aber dies ist nicht die Ende, da wiederum die Regel angewendet werden kann, um noch mehr zu produzieren! In der Tat haben Sie jetzt ein unendliches Modell!

 
{g(a,gn+1(b)), g(b, gn+1(b))} 

---

Dieses von rechts nach links lesen ist oft sehr hilfreich, wenn Sie rekursive Regeln in Prolog zu verstehen versuchen. Das Lesen von oben nach unten (von links nach rechts) ist oft ziemlich schwierig, insbesondere weil man Backtracking und allgemeine Vereinheitlichung berücksichtigen muss.

Answer 2

In Bezug auf Ihre Frage: „Da auch die Herbrand-Modelle Teilmenge der Basis Herbrand sind, wie bestimme ich die am wenigsten Herbrand-Modell durch Induktion“

Wenn Sie einen Satz P von Horn-Klauseln haben, das bestimmte Programm, dann können Sie ein Programm Operator definieren:

T_P(M) := { H S | S is ground substitution, (H :- B) in P and B S in M } 

Das Mindeste Modell ist:

inf(P) := intersect { M | M |= P } 

Bitte beachten Sie, dass nicht Alle Modelle eines bestimmten Programms sind Fixpunkte des Programmierers . Zum Beispiel ist das vollständige Herbrand-Modell immer ein Modell von das Programm P, das zeigt, dass bestimmte Programme immer konsistent sind, aber es ist nicht unbedingt ein Fixpunkt.

Auf der anderen Seite ist jeder Fixpunkt des Programmoperators ein Modell des definitiven Programms. Nämlich, wenn Sie T_p (M) = M, dann kann man M schließen | = P. So dass nach einiger weiteren mathematischen Argumentation (*) findet man, dass die am wenigsten Fixpoint ist auch das am wenigsten Modell:

lfp(T_P) = inf(P) 

Aber wir brauchen noch weitere Überlegungen, damit wir sagen können, dass wir das kleinste Modell durch eine Art Berechnung bestimmen können. Nämlich man leicht fest, dass die Programm Betreiber angrenzt, also bewahrt unendliche Gewerkschaften von Ketten, da Horn-Klauseln haben nicht forall quantifiers in ihrem Körper:

union_i T_P(M_i) = T_P(union_i M_i) 

Damit wieder nach einiger weiteren mathematischen Argumentation (*) Man findet, dass wir den kleinsten Fixpunkt über Iteration berechnen können, der für einfache Induktion verwendet werden kann. Jedes Element des kleinsten Modell hat eine einfache Ableitung von endlichen Tiefe:

union_i T_P^i({}) = lpf(T_P) 

Bye

(*) Wahrscheinlich finden Sie weitere Hinweise auf die genaue mathematische Argumentation in diesem Buch benötigt, aber leider ich kann mich nicht daran erinnern, welche Abschnitte relevant sind:
Foundations of Logic Programming, John Wylie Lloyd, 1984
http://www.amazon.de/Foundations-Programming-Computation-Artificial-Intelligence/dp/3642968287