This paper provides a set of cut-free complete sequent-style calculi for deontic STIT ('See To It That') logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting. We leverage these calculi to write a proof-search algorithm deciding deontic, multi-agent STIT logics with (un)limited choice and introduce a loop-checking mechanism to ensure the termination of the algorithm. Despite the acknowledged potential for deontic reasoning in the context of autonomous, multi-agent scenarios, this work is the first to provide a syntactic decision procedure for this class of logics. Our proof-search procedure is designed to provide verifiable witnesses/certificates of the (in)validity of formulae, which permits an analysis of the (non)theoremhood of formulae and act as explanations thereof. We show how the proof system and decision algorithm can be used to automate normative reasoning tasks such as duty checking (viz. determining an agent's obligations relative to a given knowledge base), compliance checking (viz. determining if a choice, considered by an agent as potential conduct, complies with the given knowledge base), and joint fulfillment checking (viz. determining whether under a specified factual context an agent can jointly fulfill all their duties).

翻译：本文为道义STIT（'See To It That'）逻辑提供了一套无切割的完全序列式演算，该逻辑用于在多智能体环境中对选择行为、义务与规范进行形式化推理。我们利用这些演算编写了一个判定具有（非）受限选择的道义多智能体STIT逻辑的证明搜索算法，并引入循环检查机制以确保算法的终止性。尽管道义推理在自主多智能体场景中具有公认的潜力，但本工作是首次为该类逻辑提供语法层面的判定过程。我们的证明搜索过程旨在为公式的（非）有效性提供可验证的见证/证书，从而支持对公式（非）定理性的分析并作为其解释。我们展示了如何利用该证明系统与判定算法来自动化规范推理任务，例如义务检查（即确定智能体相对于给定知识库的义务）、合规性检查（即判定智能体考虑作为潜在行为的选择是否符合给定知识库）以及联合履行检查（即在指定事实情境下判定智能体能否共同履行其全部义务）。