Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support

Off-the-shelf theorem provers and model finders for HOL are assisting the LogiKEy designer of ethical intelligent agents to flexibly experiment with underlying logics and their combinations, with ethico-legal domain theories, and with concrete examples---all at the same time.