Toward Ethical Robots via Mechanized Deontic Logic

We suggest that mechanized multi-agent deontic logics might be appropriate vehicles for engineering trustworthy robots. Mechanically checked proofs in such logics can serve to es-tablish the permissibility (or obligatoriness) of agent actions, and such proofs, when translated into English, can also ex-plain the rationale behind those actions. We use the logical framework Athena to encode a natural deduction system for a deontic logic recently proposed by Horty for reasoning about what agents ought to do. We present the syntax and seman-tics of the logic, discuss its encoding in Athena, and illustrate with an example of a mechanized proof