Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

This paper introduces Elenchus, a dialogue system that leverages prover-skeptic interactions between a human expert and an LLM to construct knowledge bases grounded in inferentialist semantics, mapping dialectical states to formal logic to explicitly capture and verify the inferential relationships and design rationales of complex ontologies like PROV-O.

The Gist

Imagine you are trying to write a rulebook for a complex game, like chess or a new video game. Traditionally, a "Knowledge Engineer" would sit down with a Grandmaster, ask them questions like, "What happens if a pawn reaches the end?" and then try to write down the rules based on the Grandmaster's answers.

The problem is that experts often don't have a perfect, pre-written rulebook in their heads. They know how to play by feeling and practice, but explaining the "why" and "what if" is hard. They might give a vague answer, or forget a weird edge case. This is the "Knowledge Acquisition Bottleneck."

Elenchus is a new way to build these rulebooks. Instead of just asking questions, it turns the process into a debate between a human expert and an AI.

Here is how it works, using some simple analogies:

1. The Setup: The "Socratic Sparring Partner"

Think of the AI not as a smart encyclopedia that knows everything, but as a Socratic sparring partner (like a debate coach).

• The Human (The Expert): Has the deep knowledge of the game. They make a claim, like "If a pawn moves forward, it captures diagonally."
• The AI (The Skeptic): Its job isn't to know the answer, but to poke holes in the expert's logic. It says, "Wait, if the pawn moves forward, but there's a wall there, does it still capture? Or what if two pawns are in the same spot?"

The AI acts as a "Defeasible Oracle." This is a fancy way of saying: "I'm going to guess where your logic might be broken. You are the boss. If I'm wrong, you tell me. If I'm right, you fix your rule."

2. The Process: Finding the "Tensions"

As they talk, the AI points out Tensions.

• Analogy: Imagine you are building a house of cards. You say, "I put a card here." The AI says, "If you put a card there, and you also put one there, the whole thing collapses."
• The expert has to fix the collapse. They can:
  • Retract: "Okay, I take that back. That rule doesn't work."
  • Refine: "Ah, I see. It only works if the card is red."
  • Contest: "No, actually, my rule is fine, and your guess about the collapse was wrong."

Every time the expert agrees that a tension is real, they are essentially saying, "Okay, I admit these two rules cannot exist together." This agreement becomes a permanent part of the new rulebook.

3. The Result: A "Living Map" of Logic

At the end of the conversation, you don't just have a list of rules. You have a Material Base.

• The Analogy: Think of a standard rulebook as a flat map. Elenchus creates a 3D topographic map. It doesn't just show you where the roads are; it shows you the relationships between them. It knows that "Road A leads to Road B," but also that "Road A breaks if you add Road C."
• This map is special because it is non-monotonic. In normal logic, if A leads to B, adding more facts usually doesn't change that. But in the real world (and in Elenchus), adding a new fact (like "It's raining") might change the outcome (the road is now closed). Elenchus captures these real-world "exceptions" naturally.

4. The Proof: The "W3C PROV-O" Test

The authors tested this on a real-world standard called PROV-O, which is like the "Constitution" for tracking where data comes from on the internet.

• They fed the AI a short, 350-word paragraph describing the rules.
• The AI and the human expert had a debate.
• The Magic: The final "rulebook" the AI helped build matched the actual design decisions made by the original team of experts years ago.
• Even better, the original team had to sift through 8,820 emails and 152 meetings to figure out their own design choices. Elenchus did it in a single dialogue session, and the resulting logic was so precise that a computer could verify it was mathematically correct.

Why This Matters

• No More "Black Boxes": In many AI systems, you don't know why the AI made a rule. In Elenchus, every single rule in the final database can be traced back to a specific moment in the conversation where the expert said, "Yes, I agree that is a problem."
• The Human is Still King: The AI can hallucinate (make things up), but because the human gets to say "No, that's wrong," the AI's mistakes are filtered out. The human remains the authority.
• Making the Implicit Explicit: Experts often know things they can't easily explain. Elenchus forces them to explain by challenging them, turning their "gut feeling" into a formal, logical structure.

In short: Elenchus is a tool that turns a messy, natural conversation between a human and an AI into a perfectly structured, mathematically verified rulebook, by treating the conversation as a game of "find the contradiction" rather than "extract the answer."

Technical Summary

Here is a detailed technical summary of the paper "Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues" by Bradley P. Allen.

1. Problem Statement

The paper addresses the persistent knowledge acquisition bottleneck in knowledge engineering. Traditional approaches treat expert knowledge as pre-existing, determinate content that must be "extracted" from experts or texts and formalized. This view assumes experts possess internal formal structures that merely need transcription. However, the author argues that knowledge is not determinate prior to articulation; rather, it is constituted through practices of expression and negotiation. Consequently, current methods struggle to formalize expert knowledge expressed in natural language because they fail to capture the dynamic, inferential nature of how experts actually reason and resolve inconsistencies.

2. Methodology: The Elenchus Protocol

The paper proposes Elenchus, a dialogue system grounded in inferentialist semantics (Brandom, Hlobil). Instead of extraction, Elenchus treats knowledge engineering as explicitation—making implicit inferential relationships explicit through dialogue.

Core Components

• Participants: A human Respondent (domain expert) and an LLM Opponent.
• The Protocol: A bilateral dialectical protocol where the Respondent develops a position (a set of commitments and denials) on a topic.
  • The Opponent's Role: Acts as a defeasible derivability oracle. It challenges the Respondent's position by proposing tensions (claims that specific combinations of commitments and denials are jointly incoherent).
  • The Respondent's Role: Resolves tensions by:
    1. Retraction: Removing a commitment or denial.
    2. Refinement: Modifying a proposition to dissolve the conflict.
    3. Contestation: Rejecting the opponent's claim of incoherence.
• State Management: The system maintains a Dialectical State $S = \langle [C:D], T, I \rangle$, where:
  • $[C:D]$ is the current position (Commitments $C$, Denials $D$).
  • $T$ is the set of open (unresolved) tensions.
  • $I$ is the set of Material Implications (accepted tensions).
• Implementation: The system is implemented as a Claude Code agent using GitHub as persistent storage. Commitments, denials, and challenges are stored as GitHub Issues, ensuring a public, versioned, and traceable record of the dialectic.

3. Key Contributions

A. Theoretical Mapping to NMMS Logic

The paper provides a formal mapping from Elenchus dialectical states to Material Bases in NonMonotonic MultiSuccedent (NMMS) logic (Hlobil and Brandom, 2025).

• Material Base Construction: The resulting knowledge base $B_S$ consists of an atomic language $L_{B_S}$ and a consequence relation $| \sim_{B_S}$.
• Containment: The mapping satisfies the Containment condition (asserting and denying the same sentence is incoherent), which is a prerequisite for the NMMS logical extension.
• Dual Components of Incoherence: The consequence relation is composed of two distinct parts:
  1. $I$ (Discovered Incoherence): Pairs derived from accepted tensions during the dialogue (substantive, dialectically discovered).
  2. $Cont$ (Structural Incoherence): Pairs where $\Gamma \cap \Delta \neq \emptyset$ (the pragmatic norm of bilateral consistency presupposed by the dialogue).
• Significance: This fills a gap in the inferentialist program by providing a computational method to generate a material base from linguistic practice.

B. Logical Elaboration via NMMS

Using the pyNMMS reasoner, the paper demonstrates how logical vocabulary (connectives like $\to, \land, \lor, \neg$) can be elaborated from the material base.

• Supraclassicality: All classically valid sequents hold.
• Conservativity: No new base-level consequences are introduced; the substructural nature (non-monotonicity, non-transitivity) of the expert's knowledge is preserved.
• Explicitation: Logical vocabulary makes explicit the material inferences already present in the base without flattening them into classical logic.

C. End-to-End Integration

The paper presents a working implementation that integrates natural language dialogue, formal state management, and automated logical reasoning, moving from unstructured expert input to a formally verified knowledge base.

4. Results: The PROV-O Case Study

The approach was tested on Section 3.1 of the W3C PROV-O provenance ontology (a 350-word prose specification).

• Process: A domain expert engaged in a dialogue with the LLM. The LLM extracted initial commitments and raised 7 challenges regarding underspecifications.
• Outcome: The dialogue converged on a final state with 19 commitments and 9 accepted material implications.
• Validation against Historical Data: The 7 challenges raised by Elenchus corresponded directly to 6 of the 7 design tensions documented in a retrospective analysis of the PROV standard (Moreau et al., 2015), which was based on 8,820 emails and 666 issues.
• Formal Verification (pyNMMS):
  • Non-transitivity: Verified that $p_2 | \sim p_{18}$ and $p_{18} | \sim p_{23}$ hold, but $p_2 | \sim p_{23}$ does not. This matches the design rationale that the core Entity concept does not automatically entail extended vocabulary.
  • Non-monotonicity: Verified that adding context (e.g., chain types) can defeat an inference (e.g., $p_7 | \sim p_{28}$ holds, but $p_7, p_{24} | \sim p_{28}$ does not), modeling the shift from "scruffy" to "proper" provenance.
  • Independence: Cross-chain queries returned false, confirming that the three views (Entity, Activity, Agent) are inferentially independent, as intended by the PROV design.
  • Retraction: A retracted commitment ($p_{20}$) left no inferential residue in the base, confirming the system's ability to handle dynamic knowledge correction.

5. Significance and Impact

• Re-conceptualizing Knowledge Engineering: Shifts the paradigm from "extraction" (transcribing static facts) to "explicitation" (negotiating inferential relationships). The knowledge base is a record of what was defended, not just what was believed.
• Handling LLM Unreliability: Instead of treating LLM hallucinations as a failure, Elenchus treats the LLM as a defeasible oracle. False positives (spurious tensions) are filtered by the human expert's contestation. The cost of error is a wasted dialogue turn, not a corrupted knowledge base.
• Traceability: Unlike knowledge bases extracted from corpora (where provenance is often opaque), every inferential relationship in Elenchus is traceable to a specific dialogue move and resolution.
• Formal Guarantees: The resulting knowledge bases possess specific structural properties (non-transitivity, non-monotonicity) that align with real-world design rationales, which can be mechanically verified.
• Future Potential: The framework offers a path toward an end-to-end inferentialist knowledge engineering system, potentially integrating with first-order extensions and scaling to larger domains via modular dialectical states.

In summary, Elenchus demonstrates that a structured, adversarial dialogue between a human expert and an LLM can generate a formally rigorous, traceable, and structurally sound knowledge base that captures the nuanced, non-monotonic reasoning of domain experts.