Proof Theory and Decision Procedures for Deontic STIT Logics

Tim LyonTim Lyon, Kees van BerkelKees van Berkel

Download

Tim Lyon, Kees van Berkel
Proof Theory and Decision Procedures for Deontic STIT Logics
Journal of Artificial Intelligence Research, to appear

Details
Bibtex

KurzfassungAbstract
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 special 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).
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{LB2024,
  author  = {Tim Lyon and Kees van Berkel},
  title   = {Proof Theory and Decision Procedures for Deontic {STIT} Logics},
  journal = {Journal of Artificial Intelligence Research},
  year    = {2024}
}