Towards a Formalisation of Justification and Justifiability

TL;DR

This paper introduces the logic QKSD, a multi-modal logic with bounded quantification, enabling formal reasoning about justifications and information components, with a comparison to Artemov's logic and a prototype solver.

Contribution

The paper formalizes QKSD, a novel logic supporting quantification over modalities, and provides a prototype satisfiability solver demonstrating its practical applicability.

Findings

QKSD allows quantification over information components.

Comparison shows similarities and differences with Artemov's logic.

Prototype solver successfully handles example formulas.

Abstract

We introduce the logic QKSD which is a normal multi-modal logic over finitely many modalities that additionally supports bounded quantification of modalities. An important feature of this logic is that it allows to quantify over the information components of systems and, hence, can be used to derive justifications. We compare the proposed logic with Artemov's justification logic and also report on a prototypical implementation of a satisfiability solver of this logic and show some examples.