Dagstuhl Seminar 23151 "Normative reasoning for AI" 2023
-
Event date:
10-Apr-2023 - 14-Apr-2023
-
Event place:
Dagstuhl, Germany
-
Keywords:
Condtitonal obligation; population ethics; Isabelle/Hol
en
Additional information:
This work lays the groundwork for a (proper) mechanisation of normative reasoning, via
the use of a so-called analytic sequent calculi. They are particularly useful for backward
reasoning and deontic explanations. To answer a question of the form “why should I do X?”,
needed is to retrieve the path (the “proof”) leading to this conclusion. Analytic calculi allow
precisely this.
This is part of a bigger project aiming at developing analytic proof systems for deontic
logic formalisms.
We consider a SoA formalism, the preference-based system E for conditional obligation
due to Aqvist. Its key strength lies in its ability to resolve the CTD paradox. We provide an
analytic calculus for it, the first of its kind. We also provide a terminating countermodel
generation procedure in case of failure of proof search, and a complexity result (co-NP
