Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
Proof Theory and Decision Procedures for Deontic STIT Logics
Authors: Tim S. Lyon, Kees van Berkel
JAIR 2024 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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 proofsearch 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. |
| Researcher Affiliation | Academia | Tim S. Lyon EMAIL Technische Universität Dresden, Nöthnitzerstraße 46, 01187 Dresden, Germany Kees van Berkel EMAIL TU Wien, Institute for Logic and Computation Favoritenstraße 9, 1040, Vienna, Austria |
| Pseudocode | Yes | Algorithm 1: Provek n Input: A Labeled Sequent: Λ = R Γ Output: A Boolean: True, False |
| Open Source Code | No | The paper discusses the design of algorithms ("We leverage these calculi to write a proof-search algorithm deciding deontic, multi-agent STIT logics") but does not provide any statement about making the code publicly available or links to a repository. |
| Open Datasets | No | The paper focuses on theoretical logical frameworks and algorithms. It does not refer to any datasets for empirical evaluation. Examples like the "Jade and Kai cycling scenario" are illustrative, not data. |
| Dataset Splits | No | No empirical datasets are used, therefore no dataset splits are discussed. |
| Hardware Specification | No | The paper describes theoretical logical frameworks and algorithms and does not contain any experimental results or mention specific hardware used for computations. |
| Software Dependencies | No | The paper describes theoretical algorithms and does not mention specific software dependencies or versions used for implementation. |
| Experiment Setup | No | The paper is theoretical, presenting logical systems and algorithms, and therefore does not describe experimental setup details or hyperparameters. |