Towards ethical robots via mechanized deontic logic
Konstantine Arkoudas, Selmer Bringsjord, Paul Bello
Abstract:
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
establish the permissibility (or obligatoriness) of agent actions,
and such proofs, when translated into English, can also explain 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 semantics of the logic, discuss its
encoding in Athena, and illustrate with an example of a
mechanized proof.
Back to the
publication list of Konstantine Arkoudas