On Quantified Modal Theorem Proving for Modeling Ethics
Naveen Sundar Govindarajulu (Rensselaer AI, Reasoning Lab), Selmer, Bringsjord (Rensselaer Polytechnic Institute), Matthew Peveler (Rensselaer, Polytechnic Institute)

TL;DR
This paper explores the use of a specialized quantified modal logic, DCEC, for modeling ethical theories in autonomous systems and proposes a proof automation approach tailored to its unique requirements.
Contribution
It introduces a fragment of DCEC and sketches an algorithm to enhance proof automation for ethical reasoning in autonomous systems.
Findings
Identifies unique proof requirements for ethical modal logics
Proposes a proof automation sketch for DCEC
Models ethical principles like double effect and virtue ethics
Abstract
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. Meeting these requirements necessitates investigation of new approaches for proof automation. Particularly, a quantified modal logic, the deontic cognitive event calculus (DCEC), has been used to model various versions of the doctrine of double effect, akrasia, and virtue ethics. Using a fragment of DCEC, we outline these distinct characteristics and present a sketches of an algorithm that can help with some aspects proof automation for DCEC.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
