Abstract
We present Elenchus, a dialogue system for knowledge base construction grounded in inferentialist semantics, where knowledge engineering is re-conceived as explicitation rather than extraction from expert testimony or textual content. A human expert develops a bilateral position (commitments and denials) about a topic through prover-skeptic dialogue with a large language model (LLM) opponent. The LLM proposes tensions (claims that parts of the position are jointly incoherent) which the expert resolves by retraction, refinement, or contestation. The LLM thus serves as a defeasible derivability oracle whose unreliability is structurally contained by the expert's authority. Our main technical contribution is a mapping from Elenchus dialectical states to material bases in Hlobil and Brandom's NonMonotonic MultiSuccedent (NMMS) logic, satisfying Containment and enabling the elaboration of logical vocabulary that makes explicit the inferential relationships negotiated in the dialectic. We demonstrate the approach on the W3C PROV-O provenance ontology, where a single dialogue session elicits and structures design tensions that a domain expert can articulate, corresponding to decisions documented in a retrospective analysis of the ontology's design. Using pyNMMS, an automated NMMS reasoner, we verify that the structural properties of the resulting material base (nontransitivity, nonmonotonicity, and independence) correspond to specific PROV design rationales, demonstrating end-to-end integration from dialogue through formal reasoning.
Abstract (translated)
我们介绍了一种名为Elenchus的对话系统，该系统旨在通过推理主义语义学构建知识库。在这个框架中，知识工程被重新定义为明确化过程，而非从专家证词或文本内容中的提取。一个领域内的专家会与大型语言模型（LLM）对手进行证明者-怀疑论者的对话，并就某个主题形成双边立场（承诺和否定）。在这一过程中，LLM提出张力（即认为该立场的部分是共同自相矛盾的主张），而专家则通过撤回、细化或反驳来解决这些张力。因此，LLM充当了一个可推翻性的推理预言机，其不可靠性被专家权威所结构化地限制。 我们的主要技术贡献在于将Elenchus辩证状态映射到了Hlobil和Brandom的非单调多后承（NMMS）逻辑中的材料基础，确保了包含原则并允许扩展逻辑词汇以明确在辩论中协商的推理关系。我们通过W3C PROV-O出处本体来展示这种方法的应用，在单一对话会话中引发了领域专家可以阐明的设计张力，并且这些张力对应于对本体设计的回顾分析中的记录决策。 利用pyNMMS（一个自动化NMMS推理器），我们验证了所得材料基础的结构性特征（非传递性、非单调性和独立性）与特定PROV设计理由相吻合，从而展示了从对话到正式推理的端到端集成。
URL
https://arxiv.org/abs/2603.06974
