Die Arbeit erweitert das Übersetzungstool anthem, um die starke Äquivalenz von Logikprogrammen mit Negation, einfachen Choices und Pools in klassischer Logik ausdrücken und verifizieren zu können.
In dieser Arbeit wird eine systematische Methode entwickelt, um klassische koalgebraische Logiken zu vielbewerteten koalgebraischen Logiken über semi-primalen Algebren zu erweitern, wobei Eigenschaften wie Ein-Schritt-Vollständigkeit und Ausdrucksstärke erhalten bleiben.
Die Arbeit untersucht, wie Bisimulationen auf zusammengesetzten Zustandssystemen aus Bisimulationen auf Teilsystemen konstruiert werden können. Der Schlüssel ist die Verwendung von Codensität-Liftings sowohl für die Verhaltensfunktoren als auch für die Strukturfunktoren, die die Komposition beschreiben.
Die Kernaussage dieses Artikels ist, dass die Mechanisierung von (präferenzbasierter) bedingter normativer Logik durch eine flache semantische Einbettung in Isabelle/HOL erreicht werden kann. Dies ermöglicht zwei Anwendungen: Zum einen als Werkzeug für Meta-Reasoning über die betrachteten Logiken, insbesondere zur automatischen Verifikation von Korrespondenzen zwischen Axiomen und semantischen Bedingungen. Zum anderen als Werkzeug zur Bewertung ethischer Argumente, wie am Beispiel des "Repugnanten Schlusses" in der Populationsethik gezeigt wird.
Der Beitrag präsentiert einen generischen Algorithmus zum exponentialzeitlichen Erfüllbarkeitsprüfen in coalgebraischen µ-Kalkülien, der auch Fälle ohne wohlverhaltenene Tableauregeln abdeckt. Dies ermöglicht neue Anwendungen wie den Presburger-µ-Kalkül und den probabilistischen µ-Kalkül mit polynomialen Ungleichungen.
Durch die Integration von Erklärungen in die Extraktion von LTL-Spezifikationen aus Demonstrationen können die Zuverlässigkeit und Relevanz der generierten Formeln erhöht werden.
Die Arbeit untersucht semantische Gegenstücke für die syntaktischen Wohlgeformtheitseigenschaften globaler Typen, nämlich Projektierbarkeit und Beschränktheit, im Modell der Prime Event Structures.
Die Arbeit entwickelt eine erweiterte Form der propositionalen dynamischen Logik (OPDL), die es ermöglicht, Nebenläufigkeit und verschiedene Operationssemantiken für Programme zu modellieren. Dies überwindet Einschränkungen früherer Ansätze zur Anwendung der propositionalen dynamischen Logik auf Nebenläufigkeit.