Der Vortrag beschaeftigt sich mit Uebersetzungsmethoden von Modallogiken in das guarded Fragment. Erstens erklaere ich die standard Uebersetzung von Modallogik K in das guarded Fragment. (Das guarded Fragment ist eine entscheidbare Teilmenge von Logik erster Stufe) Danach gebe ich eine erweiterte Uebersetzungsmethode mit der auch die Modallogik S4 uebersetzt werden kann.

Waehrend des restlichen Vortrags beschaeftige ich mich mit der Frage fuer welche Modallogiken diese erweiterte Uebersetzungsmethode verwendbar ist.

Jede Modallogik die eine regulaere Framebedingung hat, ist uebersetzbar. Aber, wenn eine Modallogik eine nicht regulaere Framebedingung hat, muss das noch nicht bedeuten dass die Logik keine Uebersetzung hat. Die meisten Logiken koennen durch mehrere Framebedingungen definiert werden. Fuer die Uebersetzung reicht es wenn eine der Framebedingungen regulaer ist.

Ich gebe eine sprachentheoretische Characterisierung die genau festliegt, wenn zwei Framebedingungen die gleiche Modallogik definieren. Danach zeige ich, dass wenn eine Modallogik eine regulaere Framebedingung hat, dass dann auch ihre maximale Framebedingung regulaer ist. Das bedeutet, dass man, wenn man wissen will ob eine Modallogik uebersetzbar ist, nur die maximale Framebedingung auf Regularitaet testen muss.

Ich habe ein Programm geschrieben das fuer die maximale Framebedingungen regulaere Automaten vorschlaegt. Diese Automaten sind mit hoher Wahrscheinlichkeit korrekt, aber der Algorithmus ist nur probabilistisch. Das Programm schlaegt fuer sehr viele Modallogiken regulaere Automaten vor, ich habe aber zur Zeit fuer die meisten keinen Korrektheitsbeweis. In der Zukunft will ich das Programm verbessern, (Die Laufzeit ist jetzt ziemlich lang), und die endgueltigen Beweise liefern dass die Automaten korrekt sind. Ich werde auch die Suche nach einem Semi-Entscheidungsverfahren, das in der Lage ist, garantiert richtige Automaten zu finden, nicht aufgeben.