Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

TL;DR

Elenchus is a dialogue-based system that constructs knowledge bases by engaging experts in prover-skeptic dialogues with LLMs, translating dialectical states into formal logical structures for provenance ontology design.

Contribution

It introduces a novel method for knowledge base construction through dialectical dialogues mapped to NMMS logic, integrating formal reasoning with expert-driven knowledge elicitation.

Findings

Successfully elicited and structured design tensions in PROV-O ontology

Verified structural properties of the knowledge base with automated NMMS reasoning

Demonstrated end-to-end integration from dialogue to formal logic verification

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.