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.

Abstract

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.

License

BSD License

Topics

Related publications

  • Parent, X., & Benzmüller, C. (2023). Normative Conditional Reasoning as a Fragment of HOL (Version 3). arXiv. https://doi.org/10.48550/ARXIV.2308.10686

Session CondNormReasHOL

Cite

× 
@article{CondNormReasHOL-AFP,
  author  = {Xavier Parent and Christoph Benzmüller},
  title   = {Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset)},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/CondNormReasHOL.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest