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.