Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset)

Xavier Parent 📧 and Christoph Benzmüller 📧

March 9, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We present a mechanisation of (preference-based) conditional normative reasoning. Our focus is on Åqvist’s system E for conditional obligation and its extensions. We present both a correspondence-theory-focused metalogical study and a use-case application to Parfit’s repugnant conclusion, focusing on the mere addition paradox. Our contribution is explained in detail in [2]. This document presents a corresponding (but sligthly modified) Isabelle/HOL dataset.


BSD License


Related publications

  • Parent, X., & Benzmüller, C. (2023). Normative Conditional Reasoning as a Fragment of HOL (Version 3). arXiv.

Session CondNormReasHOL