Mal angesehen die Semantik von T-Boxen. Wir haben also praktisch bisher mehr oder weniger nur

definitorisch agiert. Wir haben uns ein paar elementare Fakten in der Semantik klar gemacht,

aber im Wesentlichen nur uns Syntax und Semantik angesehen. Jetzt kommen also die

tatsächlichen technischen Inhalte. Wir gehen umgekehrt vor wie bei der First-Order-Logik. Wir

machen also erst Ausdrucksstärke und dann erst die Algorithmik. Deswegen, weil die Algorithmik

uns eigentlich hauptsächlich beschäftigen soll und im Gegensatz zur Prädikatenlogik,

wo ja das Resultat nur negativ war, unentscheidbar und Punkt, bekommen wir hier jetzt

Erscheidbarkeit und können also ernsthaft Gedanken über Algorithmen machen. Vorweg also wie gesagt

die Abschätzung zumindest nach oben der Ausdrucksstärke. Das nimmt dann so ähnliche

Formen an wie eben die Geschichte mit den Ehrenfeucht-Freiß-C-Spielen im Fall der

Prädikatenlogik. Die Spiele sehen hier halt ein bisschen anders aus und man kann sie insofern auch

leichter und etwas nützlicher als im Fall der Prädikatenlogik in so ein statisches Format

gießen. Das machen wir jetzt und zwar ist das Stichwort dazu Bissimilarität.

So und in der Tat wir steigen gleich ein mit einer statischen Definition. Also wir nehmen uns her,

zwei Kripke Modelle, also das i, das ich da schreibe, wird also i gleich 1 oder 2. Kripke Modelle

heißt ja Paare aus Kripke Rahmen x, i, r, i, nicht r. Das soll jetzt hier nur, also für der

Einfachheit halber machen wir jetzt also Kripke Rahmen mit nur einer Relation, also der Index i

bezieht sich hier nur darauf, dass wir zwei Kripke Rahmen haben. Diesen hier, also einen indiziert mit

eins und einen indiziert mit zwei, aber beide haben jeweils nur eine Relation. Und dann gibt es, um noch

ein Modell draus zu machen, jeweils noch eine Evaluation obendrauf. Man sieht hier schon,

für Zwecke der theoretischen oder der meta-theoretischen Behandlung schwenke ich

also grundsätzlich auf Modallogik-Opnotation um. Also die Beschreibungslogiknotationen,

die geben wir uns für die Beispiele, weil die Beispiele dann schöner aussehen als wenn man

irgendwie ein langer Indizes an irgendwelche Diamonds schreibt. Aber für Zwecke der Analyse,

sowohl der Ausdrucksstärke als auch der Algorithmik, erhalten wir uns an Modallogik-Notation.

Wenn also das hier nicht Kripke Modelle sind, dann nehmen wir uns her eine binäre Relation

zwischen den beiden Zustandsmengen. Und wir sagen, so ein Ding sei eine Simulation, wenn folgende

Bedingungen gelten. Simulation heißt das, was man denkt. Ich kann mir ja alternativ diese Kripke

Modelle, wenn ich Informatiker bin, auch als so Maschinen denken. Und oft genug ist das tatsächlich

die Sichtweise auf die ganze Geschichte. Gut, hier für Zwecke von Ontologien und Beschreibungslogik und

so ist die Sichtweise eine etwas andere, aber im Grunde kann man da völlig agnostisch sein. Also

wenn wir die Dinger mal für einen Moment als Maschinen ansehen, kann eine Maschine eine andere

simulieren, wenn sie alles machen kann, was die erste macht. So, die Reihenfolge ist hierbei,

dass die zweite die erste simuliert. Das ist manchmal von der Sprechweise hier etwas verwirrend.

So, wir sagen also eine Simulation, es sei eine Simulation, wenn es bezeugt, dass immer die zweite

Maschine das machen kann, was die erste machen kann. Was soll das heißen? Na, dass das machen kann und

sich dabei so verhält. Es sind also zwei Dinge, die da verlangt werden. Nämlich erstens, machen wir

das mit dem sich so verhalten. Erstens, was machen können heißt unter anderem eine Proposition

wahr machen. Also sprich, die zweite soll jetzt alle Propositionen wahr machen, die die erste

wahr macht, längs dieser Relation. Das heißt, alles was jetzt feucht ist, quantifiziert über

ein Paar, das in Relation steht. Also für alle Paare x, y von Zuständen, die nun unter s in

Relation stehen, gilt. Erstens, wenn also x irgendeine Proposition wahr macht, sprich, wenn also x in

v1 von p ist, dann soll folgen, y macht die Proposition auch wahr, ist also in v2 von p. Und

zweitens, so das ist also jetzt, na, y kann alles machen, was x macht im Moment. So, und das soll

sich in die Zukunft fortpflanzen. Das heißt also, es soll gelten für alle Zustände x' in x1,

die von x aus erreichbar sind. Das ist also jetzt etwas, was x machen kann. x kann zu x' gehen. So,

jetzt kann ich natürlich nicht von y verlangen, dass es auch zu x' gehen kann. Es lebt noch nicht

mal im selben Krippgeraden wie x'. Das heißt, es muss etwas Entsprechendes können. Dieses Entsprechende,

was es kann, muss eben ein y' in x2 sein. Und da soll y eben in R2 hin können. So, und nun, ja,

kann natürlich das y' zunächst mal was völlig anderes sein als das x'. Das wollen wir nicht.