  This paper addresses the automation of reasoning with deontic STIT logics by
means of proof theory. Our methodology consists of leveraging sound and
cut-free complete sequent-style calculi to write a proof-search algorithm
deciding deontic, multi-agent STIT logics with (un)limited choice. In order to
ensure the termination of our proof-search algorithm, we introduce a special
loop-checking mechanism. Despite the acknowledged potential for deontic
reasoning in the context of autonomous vehicles and other areas of AI, this
work is the first to provide a syntactic decision procedure for deontic STIT
logics. Our proof-search procedures are designed to provide verifiable
witnesses/certificates of the (in)validity of formulae, which permit an
analysis of the (non)theoremhood of formulae and act as explanations thereof.
We utilize our proof-search algorithm to address agent-based normative
reasoning tasks such as compliance checking.
