Automatische Verifikation von Äquivalenzeigenschaften in fortgeschrittenen Logikprogrammen - Bachelorarbeit
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.
Systematische Erweiterung klassischer koalgebraischer Logiken zu vielbewerteten koalgebraischen Logiken über semi-primalen Varietäten
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.
Komposition von Codensität-Bisimulationen
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.
Formalisierung und Analyse von präferenzbasierter bedingter normativer Logik mithilfe von Isabelle/HOL
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.
Effiziente Verarbeitung und Analyse von Inhalten zur Gewinnung von Erkenntnissen: Coalgebraisches Erfüllbarkeitsprüfen für arithmetische µ-Kalküle
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.
Effiziente Synthese von LTL-Spezifikationen aus Demonstrationen und Erklärungen
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.
Semantische Charakterisierung der globalen Typwohlgeformtheit
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.
Propositionale dynamische Logik und Nebenläufigkeit: Eine Analyse und Erweiterung
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.
