Table of Contents
Fetching ...

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

Bradley P. Allen

TL;DR

Elenchus is presented, 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, and the approach on the W3C PROV-O provenance ontology is demonstrated.

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.

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

TL;DR

Elenchus is presented, 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, and the approach on the W3C PROV-O provenance ontology is demonstrated.

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.
Paper Structure (39 sections, 2 theorems, 1 equation, 4 figures, 4 tables)

This paper contains 39 sections, 2 theorems, 1 equation, 4 figures, 4 tables.

Key Result

Proposition 1

$\mathfrak{B}_\mathcal{S}$ satisfies Containment.

Figures (4)

  • Figure 1: The initial portion of the Elenchus system prompt.
  • Figure 2: GitHub issues capturing the state of an Elenchus dialectic described in the case study in Section \ref{['sect:casestudies']}.
  • Figure 3: A GitHub issue capturing a challenge made by the LLM opponent in the course of an Elenchus dialectic described in Section \ref{['sect:casestudies']}.
  • Figure 4: The Elenchus agent loop

Theorems & Definitions (13)

  • Definition 1: Tension
  • Definition 2: Resolution
  • Definition 3: Material Implication
  • Definition 4: Dialectical State
  • Definition 5: Material Base
  • Definition 6: Containment
  • Definition 7: Dialectical Material Base
  • Proposition 1
  • proof
  • Remark 1
  • ...and 3 more