Proof Theory and Decision Procedures for Deontic STIT Logics

Abstract

This paper provides a set of cut-free complete sequent-style calculi for deonticSTIT(‘SeeTo It That’) logics used to formally reason about choice-making, obligations, and norms ina multi-agent setting. We leverage these calculi to write a proof-search algorithm decidingdeontic, multi-agentSTITlogics with (un)limited choice and introduce a loop-checkingmechanism to ensure the termination of the algorithm. Despite the acknowledged potentialfor deontic reasoning in the context of autonomous, multi-agent scenarios, this work isthe 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)validityof formulae, which permits an analysis of the (non)theoremhood of formulae and act asexplanations thereof. We show how the proof system and decision algorithm can be usedto automate normative reasoning tasks such asduty checking(viz. determining an agent’sobligations relative to a given knowledge base),compliance checking(viz. determining ifa choice, considered by an agent as potential conduct, complies with the given knowledgebase), andjoint fulfillment checking(viz. determining whether under a specified factualcontext an agent can jointly fulfill all their duties).