As multi-agent AI systems evolve from simple chatbots to autonomous swarms, debugging semantic failures requires reasoning about knowledge, belief, causality, and obligation, precisely what modal logic was designed to formalize. However, traditional modal logic requires manual specification of relationship structures that are unknown or dynamic in real systems. This tutorial demonstrates differentiable modal logic (DML), implemented via Modal Logical Neural Networks (MLNNs), enabling systems to learn trust networks, causal chains, and regulatory boundaries from behavioral data alone. We present a unified neurosymbolic debugging framework through four modalities: epistemic (who to trust), temporal (when events cause failures), deontic (what actions are permitted), and doxastic (how to interpret agent confidence). Each modality is demonstrated on concrete multi-agent scenarios, from discovering deceptive alliances in diplomacy games to detecting LLM hallucinations, with complete implementations showing how logical contradictions become learnable optimization objectives. Key contributions for the neurosymbolic community: (1) interpretable learned structures where trust and causality are explicit parameters, not opaque embeddings; (2) knowledge injection via differentiable axioms that guide learning with sparse data (3) compositional multi-modal reasoning that combines epistemic, temporal, and deontic constraints; and (4) practical deployment patterns for monitoring, active control and communication of multi-agent systems. All code provided as executable Jupyter notebooks.

翻译：随着多智能体AI系统从简单聊天机器人演变为自主集群系统，调试语义故障需要推理知识、信念、因果性与义务性——这正是模态逻辑旨在形式化的核心要素。然而，传统模态逻辑需要手动指定实际系统中未知或动态的关系结构。本教程展示通过模态逻辑神经网络（MLNN）实现的可微分模态逻辑（DML），使系统能够仅从行为数据中学习信任网络、因果链和规制边界。我们通过四种模态提出统一的神经符号调试框架：认知模态（信任对象）、时序模态（事件何时引发故障）、道义模态（允许执行的动作）与信念模态（如何解释智能体置信度）。每种模态均在具体多智能体场景中得到验证，涵盖从外交博弈中识别欺骗性联盟到检测大语言模型幻觉等案例，完整实现展示了逻辑矛盾如何转化为可学习的优化目标。对神经符号社区的核心贡献包括：（1）可解释的学习结构，其中信任与因果性是显式参数而非隐式嵌入；（2）通过可微分公理实现知识注入，以稀疏数据引导学习过程；（3）支持认知、时序与道义约束的组合式多模态推理；（4）面向多智能体系统监控、主动控制与通信的实用部署模式。所有代码均以可执行的Jupyter笔记本形式提供。