A formal logic for verifiable and explainable AI decision-making

The proliferation of Artificial Intelligence (AI) into critical domains necessitates robust mechanisms for verifying its decisions and rendering them explainable. Current AI paradigms, particularly deep learning, often operate as "black boxes," posing significant challenges for trust, accountability, and regulatory compliance. This paper introduces a novel formal logic, termed Decision-Centric Epistemic-Temporal Logic (DC-ETL), designed specifically to model, verify, and explain AI decision-making processes. DC-ETL integrates epistemic modalities to represent an AI agent's knowledge state, temporal modalities to capture the dynamics of decision processes, and deontic-like constructs to formalize decision justifications. We define the syntax and semantics of DC-ETL, demonstrating its capacity to formally specify properties like safety, fairness, and transparency. Furthermore, we illustrate how derivations within DC-ETL can serve as verifiable proofs of an AI's decision rationale, thereby generating human-interpretable explanations. This approach offers a pathway towards intrinsically verifiable and explainable AI, moving beyond post-hoc interpretability methods. The paper discusses the theoretical underpinnings, potential applications in high-stakes scenarios, and avenues for future development, highlighting its innovation in providing a unified logical framework for V&XAI.