On Quantified Modal Theorem Proving for Modeling Ethics

Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019) EPTCS 311, 2019, pp. In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their automated reasoners, have requirements that are different from modal logics used for other purposes, e.g. for temporal reasoning. Particularly, a quantified modal logic, the deontic cognitive event calculus (DC E C), has been used to model various versions of the doctrine of double effect, akrasia, and virtue ethics. Using a fragment of DC E C, we outline these distinct characteristics and present a sketches of an algorithm that can help with some aspects proof automation forDC E C . 1 Introduction Modal logics have been used for decades to model and study a diverse set of subjects -- e.g.