  We report some results regarding the mechanization of normative
(preference-based) conditional reasoning. Our focus is on Aqvist's system E for
conditional obligation (and its extensions). Our mechanization is achieved via
a shallow semantical embedding in Isabelle/HOL. We consider two possible uses
of the framework. The first one is as a tool for meta-reasoning about the
considered logic. We employ it for the automated verification of deontic
correspondences (broadly conceived) and related matters, analogous to what has
been previously achieved for the modal logic cube. The second use is as a tool
for assessing ethical arguments. We provide a computer encoding of a well-known
paradox in population ethics, Parfit's repugnant conclusion. Whether the
presented encoding increases or decreases the attractiveness and persuasiveness
of the repugnant conclusion is a question we would like to pass on to
philosophy and ethics.
