Not logged in. · Lost password · Register

NasaOK
Member since Nov 2015
47 posts
Subject: Übungsblatt 4, Übung 1
Hallo, ich bin gerade am Übungen wiederholen, und iwie blick ich trotz Übungsmitschrift und Skript nicht wie ich die Krit Paare bestimmen soll.

https://imgur.com/a/sgXL4Ej meine Mitschrift der Aufgabe

In der Übung haben wir die 4 Regeln Umgeschrieben, dass die Variablen Global unique sind, d.h. x kommt nur in Regel 1 vor in Regel 2 heißt es dann y in R3 dann z usw...

Dann haben wir eine Regel gesucht "die auf Context matched" und haben dann verglichen:

C(t) = Ax "Nein" (Quasi C(t) = Regel 1)

C(t) = C(Dy) (C(t) = Regel 2)

C(t) = B(zw) (R4)

dann wird auf letzeres eingegangen:
C(.) = (.)
t = B(zw) = B(Bu) = L4
sigma = [B/7, u/w]
c(t) = B(Bu)
->(3) A(DB)
->(4) Du
Diese beiden sind dann das kritische Paar

Dann wird noch eine Rechnung C(.) = B*(.) angefangen
Kritischen Paare sind dann L1 -> r1 und L2 -> r2



Ich blick nicht die Vorgehensweise nicht ganz, Woran erkenne ich denn ob eine Regel "Auf Context Matched"?

Habe auch schon bei Folien von anderen Unis geschaut aber die machen es wieder anders (zumidest soweit ich es meine zu verstehen)
Hat jemand vlt in seiner Übung eine simplere/Verständliche Strategie zum Bestimmen Kritischer Paare gezeigt bekommen?
Oder kann jemand das für mich nochmal für dumme erklären?

Würde mich über eine Antwort freuen
Titanlord
Member since Jul 2018
13 posts
+1 NasaOK
Ich lerne das gerade auch und bin mir daher noch nicht ganz sicher. Ich denke mir auch "Context Matchen" ist gemeint, dass du durch Substitution aus dem Term einer Regel, den Term der anderen Regel erzeugen kannst ( linker Term der Ersetzung ist hier relevant ). Hierbei darf aber die Substitution nicht einen ganzen Term ersetzen, d.h. du darfst eine Variable nicht durch den ganzen linksseitigen Term ersetzen.
In der Aufgabe sähe das mMn. so aus (Notation könnte falsch sein):
Vgl. Regel 1 mit Regel 1: Substitution nicht möglich
Vgl. Regel 1 mit Regel 2: Substitution nicht möglich
Vgl. Regel 1 mit Regel 3: Substitution nicht möglich
Vgl. Regel 1 mit Regel 4: Substitution nicht möglich
Vgl. Regel 2 mit Regel 3: Substitution nicht möglich
Vgl. Regel 2 mit Regel 4: Substitution nicht möglich
Vgl. Regel 3 mit Regel 4: Substitution möglich: Term 3 -> Term 4 mit o = [x -> B , y -> x]

Im Endeffekt ist der Sinn der Aufgabe nur zu lernen, wie man kritische Paare findet und einen allgemeinen Unifikator angibt.

Eine simplere Art welche zu finden, ist zu Raten. Dabei sollte man natürlich ein paar Tricks haben, z.b. nach gleicher Klammerung und nach gleichen Konstanten ausschau halten. Kritische Paare zu sich selbst findet man oft bei Verschachtelten Termen, die man dann einfach ein bisschen weiter Verschachtelt, indem man eine Variable durch eine Funktion ersetzt. Einziges Problem beim Raten: Du kannst dir nicht sicher sein, ob du alle kritischen Paare gefunden hast.

Edit:
die ersten paar nicht möglich substitutionen hab ich deiner Aussage entnommen, dass nur 3 und 4 substitutionen sind. Ich habe dies nicht weiter geprüft
This post was edited on 2019-09-17, 17:12 by Titanlord.
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen