Deontic Agency and Moral Luck

This work presents temporal STIT I/O logic, an I/O logic based on temporal
STIT logic, and documents its investigation with the proof assistant tool Isabelle/
HOL. We show how to semantically embedding temporal STIT logic as
well as the out2 operator in HOL. Implementing those embeddings and also the
already existing embedding of the out1 operator into Isabelle/HOL framework,
enables the application of higher-order automatic theorem provers for automated
reasoning tasks in temporal STIT I/O logic. Finally, we relate our logic to a more
philosophical topic called moral luck, identify which aspects of moral luck can be
studied by it, and use examples from this subject as test cases for the logic.