Resolution und Umbenennung

Bachelor Grundlagen der Logik in der Informatik
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Resolution und Umbenennung
Wenn man Resolution über Prädikatenlogik führt, muss man ja in jedem Schritt Terme unifizieren. Dabei kann es ja vorkommen, dass die Terme dieselben Variablen beinhalten, beispielsweise:
{ f(x, g(y)) } und { f(y, g(x)) }
In diesem Beispiel könnte man die Terme ja einfach mit [y / x] unifizieren, aber in dem Beispiel
{ P(x, y), ¬S(y, z)) } und { S(x, f(x)) }
müsste man eigentlich zuvor umbenennen.

Mir sind zwei Möglichkeiten bekannt, wie man diesem Problem entgegenwirken kann:

  1. Wir benennen vor jeder Unifikation gemeinsame Variablen der beteiligten Terme um.
  2. (Wurde in der Tafelübung gezeigt) Wir umbenennen jeden Term mit eigenen Variablen, z. B. für den ersten Term anstatt f(x, g(y)) entsprechend (f(x_1, g(y_1)). Danach führen wir die Resolution ohne weitere Umbenennungen aus.

Sind beide Varianten äquivalent (d. h. wenn man diese verwendet, kommt man stets zu demselben Ergebnis) und welches sollte man (vor allem im Hinblick auf die Klausur) verwenden und wie auch notieren?

LG Gabriel

3

Ich bin mir nicht sicher, ob die zweite Variante immer funktioniert. Betrachte folgendes Szenario:

   {f(x, y)}        {f(x, z)}         {f(x,y)}
      ||               ||                ||
  {f(x1, y1)}      {f(x2, z2)}       {f(x3,y3)}
         \           /   \              /
          \_________/     \____________/
               v                  v
               v                  v
         {f(x1, z2)}         {f(x3, z2)}
               \                 /
                \_______________/
                        v
                        v
                       ???

Auch wenn alle Klauseln auf einer Ebene disjunkte Namen haben kannst du trotzdem durch Mischen der vorherigen Ergebnisse wieder überlappende Namen haben.
(Ich bin mir nicht ganz sicher, ob mein Beispiel geht, oder ob der Algorithmus vorher die drei Klauseln sowieso nur zu einer gemacht hätte. Aber mit ein bisschen Anpassungsarbeit bekommt man das Beispiel sicher wieder hin.)

Ich würde Variante 1 durchziehen anstatt Variante 2 + Variante 1. Denn bei Variante 2 hast du schon mal die Gefahr, dass du zu viele Variablen im Kopf herumschwirren hast :slight_smile:
Ich weiß nicht, wie das offiziell notiert werden soll, aber ich habe das immer wie oben mit einem ‘=’ notiert. Wenn dir diese Überladung von ‘=’ zu heikel erscheint, könntest du ja ‘=_\alpha’ schreiben, denn die Klauseln sind ja implizit all-quantifiziert. Das sind aber alles nur persönliche Vorschläge.

4

Vielen Danke für die ausführliche Antwort!

Wie soll man das eigentlich notieren und muss man den Unifikator mit angeben?