Paper deep dive
Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
Bradley P. Allen
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 97%
Last extracted: 3/13/2026, 12:29:20 AM
Summary
Elenchus is a dialogue system for knowledge base construction that utilizes inferentialist semantics, where knowledge is treated as an explicit inferential relationship negotiated through prover-skeptic dialogues between a human expert and an LLM. The system maps dialectical states to material bases in NonMonotonic MultiSuccedent (NMMS) logic, allowing for the formal verification of design rationales, as demonstrated in a case study on the W3C PROV-O ontology.
Entities (4)
Relation Signals (3)
Elenchus → appliedto → PROV-O
confidence 100% · We demonstrate the approach on the W3C PROV-O provenance ontology
Elenchus → uses → NMMS logic
confidence 100% · Our main technical contribution is a mapping from Elenchus dialectical states to material bases in Hlobil and Brandom’s NonMonotonic MultiSuccedent (NMMS) logic
pyNMMS → verifies → PROV-O
confidence 90% · Using pyNMMS, an automated NMMS reasoner, we verify that the structural properties of the resulting material base... correspond to specific PROV design rationales
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2603.06974v1
- Canonical: https://arxiv.org/abs/2603.06974v1
Trouble viewing inline? Open PDF directly →
Full Text
63,316 characters extracted from source content.
Expand or collapse full text
Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues Bradley P. Allen University of Amsterdam b.p.allen@uva.nl 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 incoher- ent) which the expert resolves by retraction, refinement, or contestation. The LLM thus serves as a defeasible derivabil- ity oracle whose unreliability is structurally contained by the expert’s authority. Our main technical contribution is a map- ping from Elenchus dialectical states to material bases in Hlo- bil and Brandom’s NonMonotonic MultiSuccedent (NMMS) logic, satisfying Containment and enabling the elaboration of logical vocabulary that makes explicit the inferential re- lationships 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 deci- sions 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, demonstrat- ing end-to-end integration from dialogue through formal rea- soning. 1 Introduction Knowledge engineering—the collection of activities for for- malizing knowledge for use in information systems (Studer, Benjamins, and Fensel 1998)—has faced the knowledge ac- quisition problem—the difficulty of the formalization (Du- tilh Novaes 2012) of expert knowledge expressed in natu- ral language—since its beginning (Feigenbaum 1977). De- spite fifty years of effort across expert systems, ontology, and knowledge graph engineering, the bottleneck persists. We argue this persistence stems from a mistaken con- ception of what knowledge engineering is. Traditional ap- proaches treat expert knowledge as determinate internal con- tent awaiting extraction—as if experts have formal struc- tures in their heads that need only be transcribed (Forsythe 1993). But knowledge is not determinate prior to articu- lation; it is constituted through practices of expression and negotiation. Drawing on inferentialist semantics (Brandom 1994; Hlo- bil and Brandom 2025), we propose an alternative: knowl- edge engineering as explicitation, where the task is not to extract pre-formed content but to make explicit, through di- alogue, the inferential relationships implicit in expert prac- tice. On this view, a knowledge base is not a description of what the expert believes but a record of what has been articulated and defended through dialogue. This paper makes three contributions: • We present Elenchus, a bilateral dialectical protocol that instantiates this approach. A human respondent devel- ops a position (a set of statements) on a topic through prover-skeptic dialogue with an LLM opponent. The op- ponent challenges the respondent’s commitments and de- nials, proposing tensions (claims of incoherence); the re- spondent resolves tensions through retraction, refinement, or contestation (Section 3). • We define a mapping of Elenchus dialectical states to ma- terial bases in Hlobil and Brandom’s NonMonotonic Mul- tiSuccedent (NMMS) logic (Section 4), enabling the elab- oration of logical vocabulary via NMMS (Section 5). The mapping satisfies Containment, and its structure exhibits the explicitation pattern central to the inferentialist pro- gram: the two components of the base consequence re- lation make explicit, respectively, material incoherences discovered through dialectical examination and the prag- matic norm of bilateral consistency that the dialogue pre- supposes. This mapping fills a lacuna in the inferentialist program by providing a computational means to produce a material base from linguistic practice. • We describe a working implementation of Elenchus (Sec- tion 6) and provide a case study of its application to on- tology engineering using the W3C provenance ontology PROV-O (Section 7). Using pyNMMS, an implementa- tion of the NMMS sequent calculus, we verify that the structural properties of the resulting material base corre- spond to specific design rationales documented indepen- dently for the PROV standard (Section 8). 2 Background 2.1 Inferentialist Semantics Standard approaches to semantics are representationalist: the meaning of a sentence is given by its truth conditions. arXiv:2603.06974v1 [cs.CL] 7 Mar 2026 Inference is derivative—valid inferences preserve truth. In- ferentialism (Sellars 1953; Brandom 1994) inverts this po- sition. The meaning of a sentence is given by its inferen- tial role: what it follows from, what follows from it, and what it is incompatible with. Truth and reference are deriva- tive; they are expressive devices for making explicit infer- ential relationships already implicit in practice. For knowl- edge engineering, this inversion has a practical consequence. If meaning is inferential role, then a knowledge base is not primarily a set of sentences representing the world, but a structure capturing inferential relationships among sen- tences. What matters is not just what the expert asserts, but what follows from what according to the expert. 2.2 Material Inference Classical logic treats valid inference as formal: an argument is valid in virtue of its logical form, regardless of content. But much reasoning is material: the inference from “it is raining” to “the streets will be wet” is good not because of form but because of what the words mean. The term “material” comes from the medieval distinction between for- mal and material consequence, revived by (Sellars 1953) and developed by (Brandom 1994). Material inferences are content-dependent: “it is raining, therefore the streets are wet” is good while “it is raining, therefore the streets are dry” is bad, even though both have the same logical form (none). Inferentialists take material inference as primary. The meaning of “rain” is partly constituted by its inferen- tial connections to “wet,” “clouds,” “umbrella.” Logical vo- cabulary—”if...then,” ”and,” ”or,” ”not”—is then a tool for making explicit these material relationships. To say “if it is raining then the streets will be wet” is to endorse the material inference explicitly. 2.3 Material Bases and NMMS Hlobil and Brandom (2025) formalize this picture. A ma- terial baseB consists of an atomic language L B and a base consequence relation |∼ B . The relation Γ |∼ B ∆ holds when the position of asserting everything in Γ while denying everything in ∆ is incoherent. Material bases are substructural: |∼ B need not satisfy monotonicity (adding premises can defeat an inference) or transitivity (chains of good inferences need not compose). This suits defeasible, context-sensitive expert knowledge. One condition is re- quired: Containment, which says asserting and denying the same sentence is incoherent—the minimal coherence con- straint. From any material base satisfying Containment, the NMMS sequent calculus elaborates a logical vocabulary. The extension is supraclassical (all classically valid sequents hold), conservative (no new base-level consequences), and explicative (logical vocabulary can express any base conse- quence relation). 2.4 Prover-Skeptic Dialogues Dutilh Novaes (2020) analyzes deductive reasoning through the lens of dialogue. In a prover-skeptic dialogue, one party (the prover) defends a claim while another (the skeptic) chal- lenges it. Different configurations of cooperation and adver- sariality yield different logical properties. Following analy- sis of cooperation and adversariality in Prover-Skeptic dia- logues (Dutilh Novaes 2020; Dutilh Novaes 2025), Elenchus instantiates scenario (2): the respondent seeks to develop a defensible position, while the opponent is neutral on out- come but insists on coherence, helping rather than compet- ing. 3 The Elenchus dialectical protocol Elenchus (Allen 2025b) is a Prover-Skeptic dialogue proto- col where a human respondent develops positions through a dialogue with an LLM opponent 1 . • The opponent’s role is to challenge and probe the re- spondent’s commitments and denials, detect tensions in a position, i.e., incoherences among the respondent’s com- mitments and denials, and to maintain a database of the respondent’s commitments, denials, and material impli- cations established over the course of the dialogue. • The respondent’s role is to propose an initial commit- ment (the positum) and then resolve tensions as they arise—by retracting a commitment or denial, refining a proposition to dissolve the conflict, or contesting the op- ponent’s challenge. This is enabled by the use of a large language model as a defeasible derivability oracle: the LLM opponent proposes tensions (claims of incoherence), and the respondent’s ac- ceptance or contestation of these claims determines which material implications enter the base. 3.1 Dialectical States Elenchus works within a bilateral framework following Re- stall (2005). A position is a pair [C : D] where C is a set of commitments (assertions) and D is a set of denials. A po- sition is incoherent if one cannot be entitled to all the com- mitments in C while also being entitled to all the denials in D. Definition 1 (Tension). A tension is a sequent Γ |∼ ∆ with Γ ⊆ C and ∆ ⊆ D, asserting that the position [Γ : ∆] is incoherent. Tensions arise when a respondent’s commitments and de- nials stand in relations of implication or incompatibility: • A |∼ A (consistency): one cannot assert and deny the same proposition • A, B |∼ (contrariety): A and B cannot both be asserted • |∼ A, B (subcontrariety): A and B cannot both be denied • Γ |∼ ∆ (cross-side): committing to Γ is incompatible with denying ∆ Definition 2 (Resolution). A tension Γ |∼ ∆ is accepted when the respondent resolves it by retracting some commit- ment in Γ or some denial in ∆. It is contested when the respondent rejects the claimed incoherence. Accepting a tension constitutes endorsement of the under- lying inference: the respondent acknowledges that commit- ting to Γ while denying ∆ is indeed incoherent. 1 https://github.com/bradleypallen/elenchus Definition 3 (Material Implication). The set of material im- plications I consists of pairs (Γ, ∆) such that the respondent accepted a tension Γ|∼ ∆. Definition 4 (Dialectical State). A dialectical state is a tripleS =⟨[C : D], T, I⟩ where: • [C : D] is the current position • T is the set of open (unresolved) tensions • I is the set of material implications from accepted ten- sions 3.2 The LLM opponent as a defeasible derivability oracle A natural question: can LLMs reliably identify material inferential relationships? We claim something weaker but sufficient: LLMs can identify candidate tensions reliably enough to serve as defeasible oracles whose judgments are subject to human override. This is supported by empirical findings. LLMs can func- tion as classifiers-as-intensions, applying intensional defini- tions via zero-shot prompting (Allen 2025a). They can artic- ulate rationales for classifications, surfacing inferential con- nections (Allen and Groth 2025a; Allen and Groth 2025b). And they can report bilateral doxastic states—commitment, denial, uncertainty—enabling coherence checking (Allen et al. 2025). The key is defeasibility. The LLM proposes ten- sions; the respondent accepts or contests. Only accepted ten- sions enter I . False positives are filtered by contestation; the human retains authority. The LLM surfaces candidate rela- tionships the respondent might not have considered, while the respondent determines which actually hold. The cost structure of oracle errors is asymmetric by de- sign. False positives (spurious tensions) are filtered by con- testation at the cost of a wasted dialogue turn. False nega- tives (missed tensions) are a more substantive concern ad- dressed in Section 10.3; however, the case study in Section 7 suggests that even a single dialogue session can structure expert knowledge into a material base whose implications correspond to documented design decisions. 4 From dialectical state to material base 4.1 Definitions Following Chapter 3 of Hlobil and Brandom (2025): Definition 5 (Material Base). A material baseB = ⟨L B ,|∼ B ⟩ consists of an atomic language L B and a base consequence relation|∼ B ⊆P(L B )×P(L B ). The relation Γ |∼ B ∆ holds iff the sentences in Γ are jointly a reason for those in ∆; equivalently, the position [Γ : ∆] is incoherent. Definition 6 (Containment). A material base satisfies Con- tainment iff Γ|∼ B ∆ whenever Γ∩ ∆̸=∅. 4.2 Mapping Definition 7 (Dialectical Material Base). Given a dialecti- cal state S = ⟨[C : D], T, I⟩, defineB S = ⟨L B S ,|∼ B S ⟩ by: L B S = C∪ D |∼ B S = I ∪ Cont where Cont =⟨Γ, ∆⟩ : Γ, ∆⊆ L B S and Γ∩ ∆̸=∅. Proposition 1.B S satisfies Containment. Proof. By construction, Cont⊆|∼ B S . The simplicity of this proof warrants explanation. The base consequence relation |∼ B S has two components, and their union satisfies Containment because Cont is included by definition. But the two components are not arbitrary — they have distinct origins that correspond to a distinction central to the inferentialist program. I consists of material implications produced through di- alectical examination. Each element of I originated as a tension proposed by the opponent and accepted by the re- spondent. These are discovered incoherences: the respon- dent learned, through the dialectic, that certain combina- tions of commitments and denials cannot be jointly main- tained. When the opponent maintains bilateral consistency (C ∩ D = ∅), every element of I has Γ∩ ∆ = ∅ — the protocol produces only pairs with disjoint sides. Cont con- sists of all pairs ⟨Γ, ∆⟩ with Γ ∩ ∆ ̸= ∅. These are not discovered through the dialectic. No respondent needs to be shown that asserting and denying the same sentence is inco- herent. This is a precondition of rational participation in the dialogue — a pragmatic norm that both parties accept before the first move. Cont formalizes this norm as a component of the consequence relation. The two components are therefore structurally disjoint when the dialogue is well-formed: I contains pairs with dis- joint sides (substantive, examined incoherences) and Cont contains pairs with overlapping sides (the background norm of bilateral consistency). Their union satisfies Containment not as an artifact of construction but because the material base makes explicit two kinds of incoherence: what the dia- logue produced and what the dialogue presupposed. This is an instance of the explicitation pattern that Bran- dom takes as characteristic of logical vocabulary. Just as NMMS logical connectives make explicit the material infer- ential relationships in the base, the construction of the base itself makes explicit the pragmatic norm governing the dia- logue from which the base was derived. Remark 1. The components of|∼ B S have distinct statuses: Cont is structural and I is respondent-endorsed. A looser construction might include T , representing not only what the respondent accepts but also what is claimed. T governs the dialogue dynamics while I governs the formal semantics. As a tension in T is resolved, it results in an addition to I . Remark 2. In practice, the opponent typically identifies ten- sions between small sets of propositions, often of the form A |∼ B. When accepted tensions have singleton conclu- sions, material implications are unambiguous. The frame- work accommodates the general case Γ |∼ ∆, where ac- ceptance establishes that the position [Γ : ∆] is incoherent without isolating a single conclusion. 4.3 Traceability A distinctive feature of Elenchus output is complete trace- ability. Every material implication in I originated as a ten- sion proposed by the opponent and accepted by the respon- dent. The dialogue transcript records when the tension was raised, what position prompted it, and how the respondent resolved it. This contrasts with knowledge bases extracted from cor- pora, where provenance may be opaque or statistical. In Elenchus, every inferential relationship has a dialogical jus- tification: the respondent explicitly acknowledged that these commitments and denials are jointly incoherent. 5 From material base to logical vocabulary The mapping established in Section 4 shows that Elenchus dialectical states yield material bases satisfying Contain- ment. By the results of Hlobil and Brandom (2025), the NMMS sequent calculus can elaborate logical vocabulary from these bases. This section characterizes what the logical extension provides, distinguishes it from classical approxi- mations, and discusses current limitations. Proposition 2. The logical extension ofB S via NMMS: 1. includes all classically valid sequents 2. is a conservative extension of|∼ B S 3. provides vocabulary to make explicit any reason relation in|∼ B S Proof. From Facts 2, 3, and 5 in Hlobil and Brandom (2025), which follow from Containment. Given a material baseB S satisfying Containment, NMMS elaborates logical vocabulary—connectives (→ ,∧,∨,¬)—that can make explicit any consequence relation in the base. The resulting extended consequence relation|∼ has three properties: 1. Supraclassicality: All classically valid sequents hold in |∼ 2. Conservativity: No new consequences are introduced at the base level. If Γ∪∆⊆ L B S , then Γ|∼ ∆ iff Γ|∼ B S ∆ 3. Explicitation: If Γ |∼ B S ∆, this can be expressed using logical vocabulary Crucially, conservativity means the substructural charac- ter of the material base is preserved. The base consequence relation remains nonmonotonic and nontransitive even af- ter logical vocabulary is introduced. The logical vocabulary lets us say that a material inference holds—for instance, that commitment to ”it is raining” is incompatible with denial of ”the streets are wet”—without flattening that relationship into a classical conditional that participates in monotonic reasoning. The material baseB S already constitutes a knowledge base in the inferentialist sense: a set of propositions together with a consequence relation capturing which positions are incoherent. The logical extension via NMMS enriches this with explicit logical vocabulary while preserving the sub- structural character of the base—but the material base it- self is the primary output of the Elenchus protocol, and it Figure 1: The initial portion of the Elenchus system prompt. is this structure that we claim as the knowledge base gener- ated from dialogue. 6 Implementation Elenchus is implemented as a Claude Code (Anthropic 2025) agent that maintains dialectical state across sessions using GitHub as persistent storage. Figure 1 shows the be- ginning of the CLAUDE.md prompt, a 786-line Markdown document defining the dialogue protocol in detail, including role definitions, principles for conduct of the dialogue, the specification of the commitment store, and explicit instruc- tions for each type of dialogue move 2 . Given Claude Code’s support for tool use through bash command line interface calls, this prompt suffices to completely define the behavior of the LLM opponent. The state of a dialectical engagement is stored persistently in a GitHub repository. Commitments, denials, challenges, and tensions are represented as GitHub issues (GitHub 2025) with corresponding labels, providing a browsable, versioned record of the dialectic. The agent loop (Figure 4) orchestrates the interaction: the respondent proposes speech acts (commitments, denials, tension responses), the oppo- nent (the LLM) checks coherence against the current bilat- eral state, proposes tensions when incoherence is detected, and records state transitions to the repository. Figure 2 shows the state of the dialectic discussed in Section 7, and Figure 3 shows a specific challenge made by the opponent in the context of that dialectic. This architecture choice reflects the dialogical character 2 https://github.com/bradleypallen/elenchus/blob/main/ CLAUDE.md Figure 2: GitHub issues capturing the state of an Elenchus dialectic described in the case study in Section 7. of the framework. The dialectical state is not a hidden data structure but a public record: every commitment, denial, challenge, and tension is individually addressable (as an is- sue), annotatable (via comments), and traceable (via GitHub issues history). The respondent can review the full state at any point by browsing the repository. The opponent can re- construct context across sessions by loading the current state from the repository at the start of a new session (line 1 of Figure 4). The LLM serves two functions: conversational partner (interpreting the respondent’s natural language contributions and generating challenges) and bookkeeper (maintaining the formal dialectical state and detecting candidate tensions). These roles are specified in a system prompt that instructs the agent to operate according to the Elenchus protocol, in- cluding the bilateral structure of positions, the typology of speech acts, and the requirement that tensions be proposed rather than imposed. Figure 4 specifies the Elenchus agent loop. At the start of each session, the agent loads the current dialectical state from the GitHub repository (line 1). The main loop waits for the respondent’s speech act (line 3). Commitments and denials update the position and trigger coherence checking, which may surface new tensions (lines 4–7). Tension re- sponses update the state differently depending on their type: retractions and refinements modify the position and move the tension to I as an accepted material implication (line 9); contestations remove the tension from T (line 10). After each state change, the updated state is recorded to the repos- itory (line 13). The opponent may also proactively raise So- cratic challenges—questions that probe underspecification or implicit commitments without asserting a specific tension Figure 3: A GitHub issue capturing a challenge made by the LLM opponent in the course of an Elenchus dialectic described in Sec- tion 7. (line 14). The loop is designed for asynchronous interaction. Ses- sions can be interrupted and resumed; the GitHub-backed state ensures continuity. Multiple sessions contribute to the same dialectical state, and the full history of state transitions is preserved in the GitHub issues database for the repository. The mapping from natural language dialogue moves to formal propositions and material implications is performed automatically using Python scripts: when a tension is ac- cepted, the agent records the corresponding material impli- cation without manual formalization by the respondent or a separate knowledge engineer. 7 Case study: the PROV-O ontology To demonstrate Elenchus on a knowledge representation task, we apply it to Section 3.1 (“Starting Point Terms”) of the W3C PROV-O Recommendation (Lebo, Sahoo, and McGuinness 2013), which defines three core classes (Entity, Activity, Agent) and ten properties relating them. The input is the 350-word prose specification only— examples, Turtle code, and figures are excluded. 3 The respondent (a domain expert who served as a princi- pal member of the W3C Provenance Incubator Group and co-editor of the PROV family of specifications) feeds the Section 3.1 prose to the opponent, which extracts 10 initial commitments covering class definitions, property groups, 3 https://github.com/bradleypallen/prov-o-section-3.1 1: Load dialectical state⟨[Γ : ∆], T, I⟩ from GitHub 2: while session active do 3:Wait for respondent’s speech act ▷ commitment, denial, tension response 4:if commitment (+P ) or denial (−P ) then 5:Update position; check coherence 6:if tension detected then add to T as sequent X |∼ Y ▷ X ⊆ Γ, Y ⊆ ∆ 7:end if 8:else if resolves tension X |∼ Y ∈ T then 9:if retraction or refinement then update [Γ : ∆]; move X |∼ Y to I 10:else if contestation then remove X |∼ Y from T 11:end if 12:end if 13:Record state to GitHub 14:if should probe then raise Socratic challenge 15:end if 16:Display open tensions T and challenges 17: end while Figure 4: The Elenchus agent loop temporal bounds, and provenance chain structure (Table 1). The granularity of atomic propositions is determined by the LLM opponent during extraction and is subject to the same retraction and refinement mechanisms as any commitment. The opponent then raises 7 challenges probing underspec- ifications in the prose—points where the specification says enough to prompt a question but not enough to answer it. Table 2 summarizes the completed dialectic. Seven chal- lenges were raised and resolved, yielding a final state S f = ⟨[C 19 : ∅],∅, I 9 ⟩ with 19 commitments, no denials, no open tensions, and 9 accepted material implications. The dialec- tic converged on a pragmatist interpretation of PROV-O in which ontological categories serve as modeling tools rather than metaphysical commitments. Moreau et al. (Moreau et al. 2015) reconstruct, post hoc, the requirements and design decisions behind PROV from the working group’s record of 8820 emails, 666 issues, and 152 teleconferences, identifying 73 requirements across nine themes. Six of the seven Elenchus challenges corre- spond directly to documented design tensions (Table 1). The requirements not surfaced are almost entirely outside the scope of Section 3.1. Onecommitmentwasretractedduringthedi- alectic.The respondent initially committed to p 20 : “wasDerivedFrom suffices for cross-context Entity iden- tity.” Subsequent challenges revealed that alternateOf is an equivalence relation and specializationOf a strict partial order with attribute inheritance—properties that wasDerivedFrom cannot express, since it is not even transitive. In response to the opponent’s challenge, the respondent remembered that p 20 was extended in another document, retracted p 20 and committed to p 23 : “Expanded Terms add expressiveness, not just convenience.” While not quite an instance of discovery, it is more than simply restructuring the claims in the initial set of commitments. This case study tests the protocol’s ability to structure and formalize expert knowledge, not to surface tensions invisible to the expert. Testing discovery (tensions the expert hadn’t previously considered) would require a different experimen- tal design — perhaps an expert in a related but distinct do- main, or a less experienced practitioner. We leave that type of evaluation to future work. 8 Reasoning over the material base with pyNMMS The preceding case study demonstrates that an Elenchus di- alogue can produce a material base from expert knowledge. However, Section 5 established that material bases satisfy- ing Containment admit a logical extension via NMMS with supraclassicality, conservativity, and explicitation proper- ties. To verify that these properties hold for the PROV-O ma- terial base and to probe its design-rationale structure, we use pyNMMS (Allen 2026), an open-source implementation of an automated reasoner for the NMMS sequent calculus de- fined in Chapter 3 of Hlobil and Brandom (2025). 4 The rea- soner performs root-first backward proof search with mem- oization over material bases, supporting queries over both atomic sequents and sequents involving the NMMS logical vocabulary (→,∧,∨,¬). 8.1 Base-level and structural properties Table 3 summarizes the base-level and structural results. All nine material implications from Table 2 are derivable. The base is nontransitive: p 2 |∼ p 18 and p 18 |∼ p 23 are both derivable, but p 2 |∼ p 23 is not. The base is nonmono- tonic: p 2 |∼ p 18 holds, but p 2 , p 23 |∼ p 18 does not—adding p 23 to the antecedent defeats the inference. All nine ma- terial implications are individually expressible as NMMS conditionals via the Deduction-Detachment Theorem (e.g., |∼ p 2 → p 18 ). Classical tautologies hold by supraclassi- cality (e.g., |∼ p 2 ∨¬p 2 ). The logical extension is conser- vative: introducing logical vocabulary does not create new base-level consequences. 8.2 Design rationale correspondence Table 4 presents the central result: each structural property of the material base corresponds to a specific design ratio- nale documented in Moreau et al. (Moreau et al. 2015). We highlight five correspondences. Core/extended boundary (EZ3). The nontransitivity of the Entity chain models Moreau et al.’s requirement that PROV have a minimal core with additional extensions. Both p 2 |∼ p 18 (Entity entails individuation) and p 18 |∼ p 23 (individuation entails Expanded Terms) are derivable, but p 2 |∼ p 23 is not: the core Entity concept does not auto- matically pull in extended vocabulary. The hypothetical syl- logism (p 2 → p 18 ) ∧ (p 18 → p 23 ) → (p 2 → p 23 ) is derivable by supraclassicality—it is a classical tautology— but p 2 → p 23 alone is not. Logical vocabulary can state that the chain is classically valid without enabling detachment at the base level: the core/extended boundary is preserved. 4 https://pypi.org/project/pyNMMS/ Issue #CommitmentProposition 1Three core classes form the basis of PROV-O: Entity, Activity, Agentp 1 2Entity is a thing with fixed aspectsp 2 3Activity is something that occurs over time and acts upon or with entitiesp 3 4Agent bears responsibility for activities, entities, or other agents’ activitiesp 4 5 used and wasGeneratedBy relate Activities to Entitiesp 5 6 wasInformedBy provides Activity-to-Activity dependencyp 6 7 wasDerivedFrom expresses Entity-to-Entity transformationp 7 8 wasAssociatedWith and wasAttributedTo ascribe Agent responsibilityp 8 9 actedOnBehalfOf expresses delegation with shared responsibilityp 9 10Three types of provenance chains: Activity-Entity, Activity-only, Entity-onlyp 10 Table 1: The initial commitments in the PROV-O dialectic leading to atomic propositions in the material base. Commitments were extracted from the Section 3.1 prose. Issue #Challenge(Moreau et al. 2015)ResolutionPropositionMaterial Implication 11Fixed aspects; entity change?RE1, RE3, RE5, RE6, EZ1Pragmatist: context-relative individuationp 18 p 2 |∼ p 18 12Activity duration; instants?EV1, EV4Durational activities; instantaneous eventsp 27 p 3 |∼ p 27 13Responsibility vs. causation?XG5, VI2–4, GE1Agency is pragmatic ascriptionp 29 p 4 |∼ p 29 14 wasInformedBy: shortcut?VI1, VI6, EZ1Independent: inferred, not reduciblep 30 p 6 |∼ p 30 15Derivation criteria; identity?XG8, VI5, VI6Broad causal dependencies; subtypes narrowp 28 p 7 |∼ p 28 16Delegation responsibility?XG11 (partial)Hierarchical and transitivep 25 , p 26 p 9 |∼ p 25 , p 9 |∼ p 26 17Chain types equivalent?VI1, VI6No; wasDerivedFrom requires assertionp 24 p 10 |∼ p 24 18Individuation⇒ Expanded(from #11 follow-up)Expanded Terms add expressivenessp 23 p 18 |∼ p 23 Table 2: Challenges and responses in the PROV-O dialectic leading to additional atomic propositions and material implications in the material base. Each challenge targeted an underspecification in the Section 3.1 prose; six of seven correspond to design tensions documented in Moreau et al.’s retrospective requirements analysis. The final column shows accepted material implications in I . QueryResult Base consequences (all 9 derivable) p 2 |∼ p 18 , p 3 |∼ p 27 , p 4 |∼ p 29 , p 6 |∼ p 30 True p 7 |∼ p 28 , p 9 |∼ p 25 , p 9 |∼ p 26 , p 10 |∼ p 24 , p 18 |∼ p 23 True Nontransitivity p 2 |∼ p 18 and p 18 |∼ p 23 True p 2 |∼ p 23 False Nonmonotonicity p 2 |∼ p 18 True p 2 , p 23 |∼ p 18 False p 9 |∼ p 25 True p 9 , p 26 |∼ p 25 False Explicitation (DDT) |∼ p 2 → p 18 . . . |∼ p 18 → p 23 (all 9)True |∼ p 2 → p 23 False Supraclassicality |∼ p 2 ∨¬p 2 True p 2 ∧¬p 2 |∼True Conservativity p 2 |∼ p 23 (still nontransitive)False p 2 , p 23 |∼ p 18 (still nonmonotonic)False Table 3: Structural properties of the PROV-O material base veri- fied by pyNMMS. All nine base consequences are derivable; the base is nontransitive and nonmonotonic; all base consequences are expressible as NMMS conditionals; the logical extension is supra- classical and conservative. Derivation non-transitivity (VI5). Moreau et al. docu- ment ISSUE-612 as one of the most debated PROV design decisions: derivation is not mandated to be transitive. The material base enforces this structurally. p 7 |∼ p 28 (deriva- tion entails broad causal dependency) is derivable, but p 28 does not compose with other chains. The nontransitivity is not a policy annotation but a property of the consequence relation itself. Three-views independence (VI1, GE1). The three PROV views—data flow (Entity), process flow (Activity), and re- sponsibility (Agent)—correspond to independent inference chains in the material base. All eight cross-view queries (e.g., p 2 |∼ p 27 , p 3 |∼ p 29 , p 4 |∼ p 18 ) return False. No inference leaks between views. Scruffy-to-proper refinement (EZ1). Moreau et al. de- scribe the progressive refinement from “scruffy” provenance (simple assertions) to “proper” provenance (qualified with activities, usages, and generations). Nonmonotonicity mod- els this: p 7 |∼ p 28 (derivation entails broad causal depen- dency) holds on its own, but p 7 , p 24 |∼ p 28 does not—adding chain-type context (proper detail) defeats the scruffy infer- ence. Retraction leaves no trace (GE3). The commitment p 20 (“wasDerivedFrom suffices for cross-context Entity identity”) was retracted during the dialectic. The mate- rial base records only defended commitments: p 7 |∼ p 18 , p 7 |∼ p 23 , and p 28 |∼ p 18 are all non-derivable, confirming that the retracted commitment left no inferential residue. 8.3 Pairwise independence of design resolutions The composite results confirm that the material base is well- structured as a system of design decisions. We define seven chain groups corresponding to the seven challenges in Ta- ble 2: Entity (p 18 , p 23 ), Activity (p 27 ), Agent (p 29 ), wasInformedBy (p 30 ), wasDerivedFrom (p 28 ), delega- tion (p 25 , p 26 ), and chain-type (p 24 ). Testing all cross- chain pairs yields 34 pairs, all non-derivable: every design resolution from one challenge is inferentially independent of every resolution from every other challenge. This confirms that each Elenchus challenge addressed a genuinely distinct design tension, and that the material base preserves this dis- tinctness. RequirementQueryResultProperty EZ3p 2 |∼ p 23 FNontrans. EZ3|∼(p 2 →p 18 )∧(p 18 →p 23 )→(p 2 →p 23 )TSupraclass. EZ3|∼ p 2 → p 23 FNontrans. VI5p 7 |∼ p 28 TBase VI5p 28 |∼ p 7 FDirectional VI1p 2 |∼ p 27 , p 2 |∼ p 29 FIndep. VI1p 3 |∼ p 18 , p 3 |∼ p 29 FIndep. VI1p 4 |∼ p 18 , p 4 |∼ p 27 FIndep. VI1p 7 |∼ p 30 , p 6 |∼ p 28 FIndep. EZ1p 7 |∼ p 28 TBase EZ1p 7 , p 24 |∼ p 28 FNonmon. XG11p 9 |∼ p 25 , p 9 |∼ p 26 TMulti-succ. XG11p 9 , p 25 |∼ p 26 FNonmon. EV1p 3 |∼ p 27 TBase EV1p 3 |∼ p 18 , p 3 |∼ p 25 FIndep. GE3p 7 |∼ p 18 , p 7 |∼ p 23 FRetraction GE3p 18 |∼ p 23 TActual path Table 4: Design rationale queries mapping NMMS reasoning re- sults to requirements documented in Moreau et al. (2015). Each row shows a query against the PROV-O material base, its result, and the structural property it demonstrates. F = False (non-derivable), T = True (derivable). Containment is verified for all propositions: p |∼ p holds for every p ∈ L B S , confirming that the base satisfies the minimal coherence constraint required for the NMMS logi- cal extension. 8.4 Discussion These results show how Elenchus can support an end-to- end workflow from natural language dialogue through ma- terial base construction to formal reasoning over the log- ical extension. The structural properties of the material base—nontransitivity, nonmonotonicity, conservativity, and independence—are not merely formal curiosities. They cor- respond to specific, well-documented design decisions in the PROV standard. The material base produced by a single Elenchus dialogue session over a 350-word prose specifi- cation yields a formal artifact whose properties can be me- chanically verified and whose structure aligns with decisions reconstructed by Moreau et al. from 8820 emails, 666 issues, and 152 teleconferences. The explicitation results demonstrate the pattern central to the inferentialist program: logical vocabulary makes ex- plicit what is already implicit in the material base. Each design decision can be expressed as an NMMS conditional (|∼ p 2 → p 18 ), and the conjunction of these conditionals can be stated, but the logical vocabulary does not alter the base-level consequence relation. The core/extended bound- ary (EZ3) provides a particularly clear illustration: the hy- pothetical syllogism is derivable by supraclassicality, yet the transitive collapse is not—logical vocabulary can describe the chain without collapsing it. 9 Related work 9.1 Knowledge acquisition methods Knowledge acquisition has been studied since the earliest expert systems. The ”knowledge acquisition bottleneck” was identified by Feigenbaum (1977) and has motivated decades of work on structured elicitation methods including repertory grids (Boose 1985), protocol analysis (Ericsson and Simon 1984), and ontology learning from text (Cimi- ano 2006). CommonKADS (Schreiber et al. 2000) pro- vides a comprehensive methodology treating knowledge en- gineering as modeling, not mining—a perspective Elenchus shares.However, CommonKADS and related method- ologies (METHONTOLOGY (Fern ́ andez-L ́ opez, G ́ omez- P ́ erez, and Juristo 1997), NeOn (del Carmen Su ́ arez de Figueroa Baonza 2010)) assume the target is a description of the domain in a formal language, with the knowledge en- gineer mediating between expert and formalism. Elenchus eliminates this mediating step: the expert interacts directly with the opponent through natural language, and the formal structure (the material base) is constructed as a byproduct of the dialogue. The Socratic method has been applied to knowledge elicitation before. SHAKEN (Clark et al. 2001) used structured dialogue to acquire knowledge from sub- ject matter experts, and the Knowledge Machine (Clark and Porter 1997) employed question-driven elicitation. These systems, however, treat the acquired knowledge representa- tionally—the dialogue is a means to extract content that is then encoded in a pre-existing formalism. Elenchus treats the dialogue as constitutive: the material base just is the structured record of commitments, denials, and accepted material implications from the dialogue. 9.2 LLMs for knowledge base construction Recent work has explored LLMs for ontology construction (Babaei Giglou, D’Souza, and Auer 2023), knowledge graph completion (Yao et al. 2025), and information extraction (Wei et al. 2023). These approaches typically use LLMs to generate triples, axioms, or class hierarchies, treating the LLM as a source of knowledge to be validated. The qual- ity concern is well-documented: LLMs hallucinate, con- fabulate, and produce plausible but incorrect formalizations. Elenchus takes a fundamentally different stance. The LLM is not a source of knowledge but a dialectical partner—a de- feasible derivability oracle that proposes candidate tensions for the respondent to accept or contest. The respondent, not the LLM, is the epistemic authority. This design transforms the hallucination problem from a reliability issue into a fea- ture of the protocol: an LLM-proposed tension that does not reflect genuine incoherence is simply contested by the re- spondent, and the contestation itself is part of the dialectical record. False positives are filtered; the cost of hallucination is at most a wasted challenge, not a corrupted knowledge base. This contrasts with neurosymbolic approaches (Allen et al. 2025) where LLM unreliability is managed through paraconsistent reasoning (Belnap 1977). In Elenchus, LLM unreliability is structurally contained by the respondent’s au- thority over (and accountability for) tension resolution. 9.3 Argumentation frameworks Elenchus shares surface structure with computational argu- mentation. Dung’s (1995) abstract argumentation frame- works define conflict relations over arguments; ASPIC+ (Modgil and Prakken 2014) provides structured argumen- tation with defeasible and strict rules; and dialogue-based argumentation protocols (Prakken 2006) formalize multi- agent debate. The relationship to Elenchus requires care- ful differentiation along three dimensions. First, the con- sequence relation. In standard argumentation frameworks, the consequence relation (what follows from what) is fixed in advance—typically classical logic or a specified defea- sible logic. In Elenchus, the consequence relation is itself the output. Second, the role of the opponent. In adver- sarial argumentation, the opponent seeks to defeat the pro- ponent’s arguments. This is closer to the proof-checking role of the skeptic in dialogical logic (Lorenzen and Lorenz 1978) than to an adversary in a debate. Third, the output. Argumentation frameworks produce extensions (sets of ac- ceptable arguments) or labelings. Elenchus produces a ma- terial base—a substructural consequence relation that can serve as input to the NMMS sequent calculus. This connects knowledge acquisition directly to the inferentialist program in philosophical logic, rather than to the argumentation the- ory tradition. That said, there is productive overlap. Bipolar argumentation frameworks (Cayrol and Lagasquie-Schiex 2005), which include both attack and support relations, have structural affinity with bilateral positions. And the connec- tion between argumentation-based dialogue and nonmono- tonic reasoning (Governatori et al. 2004) suggests that ex- isting computational argumentation infrastructure could be leveraged in implementing Elenchus. The key theoretical distinction remains: Elenchus constructs the consequence relation rather than reasoning within a pre-given one. The distinction from computational argumentation is not merely one of emphasis. Dialogic logic formalizations in the Lorenzen-Lorenz tradition operate at a level of abstraction remote from realistic human dialogical practice; Elenchus follows Dutilh Novaes’s prover-skeptic analysis, which is situated in the cognitive and social roots of reasoning rather than in formal dialogue semantics. The relevant comparison is not with argumentation frameworks that adjudicate con- flicts among pre-existing arguments, but with the question of how a consequence relation comes to be constructed in the first place. 9.4 LLM-assisted ontology engineering systems Much recent work in LLM-assisted ontology engineering has centered on competency questions (CQs), natural lan- guage questions that express an ontology’s functional re- quirements (Gr ̈ uninger and Fox 1995). OntoChat (2024) is a conversational framework that uses LLMs to support on- tology requirements elicitation through four functions: user story creation, CQ extraction, CQ filtration and clustering, and ontology testing via verbalization. Zhao et al. (2024) extend OntoChat with participatory prompting, addressing the finding that domain experts struggle to prompt LLMs effectively without researcher mediation. RevOnt (Ciroku et al. 2024) reverses the traditional CQ workflow, using lan- guage models to extract competency questions from existing knowledge graphs rather than eliciting them from experts — demonstrating that RDFS-level knowledge graphs con- tain sufficient structure to reconstruct requirements. Most recently, Koutsiana et al. (2024) report an ethnographic study of knowledge engineers working with generative AI at a hackathon, finding that LLMs can improve efficiency in knowledge graph construction but that prompting is an un- dervalued skill and evaluation of LLM outputs remains the central challenge. Kampars et al. (2025) extend the NeOn methodology with LLM-based automation while retaining domain expert-in-the-loop validation.Garijo Verdejo et al. (2024) survey the landscape of LLM applications to on- tology engineering tasks, finding that most work targets early development phases. In all these systems, the LLM serves as a facilitator or generator: it elicits requirements, produces ontology frag- ments, or suggests competency questions, and the expert val- idates the output. This workflow inherits the representation- alist assumption discussed in Section 1. The expert is treated as a source — of user stories, of competency questions, of validation judgments — rather than as an agent whose com- mitments are tested for coherence. Elenchus inverts this re- lationship: the LLM challenges the expert’s commitments, and the expert’s responses to those challenges constitute the knowledge base. The formal outputs also differ in a way that goes beyond format. Competency questions and OWL fragments lack a formal characterization of what makes them collectively a knowledge base: there is no characterized consequence relation, no proven structural properties, and no system- atic traceability from output to the process that produced it. Elenchus produces material bases satisfying Containment, with proven supraclassicality, conservative extension, and explicitation properties, and complete traceability of every material implication to a specific dialogue move. The CQ- based approach evaluates its outputs through user satisfac- tion; Elenchus evaluates its outputs through formal logic. Several challenges identified in this programme are ad- dressed structurally by Elenchus. The finding that require- ments elicitation is the activity most in need of computa- tional support (Zhang et al. 2024) motivates Elenchus di- rectly, though it reconceives the task as dialectical examina- tion rather than content generation. The finding that experts struggle to prompt LLMs effectively and need structured mediation (Zhao et al. 2024) is addressed by the prover- skeptic protocol: the expert responds to challenges rather than formulating prompts, and the bilateral position frame- work constrains the interaction without requiring the expert to understand the underlying formalism. The finding that evaluation of LLM outputs is the central difficulty (Kout- siana et al. 2024) is dissolved by the Elenchus architecture: the LLM proposes tensions rather than generating artifacts, and the expert’s acceptance or contestation is the evaluation. 9.5 Multi-agent debate frameworks for improving LLM reasoning Irving et al. (2018) propose AI safety via debate, in which two AI agents argue before a human judge; the adversar- ial structure is intended to make the correct answer easier to identify than to generate. Li et al. (2024) and Liang et al. (2024) instantiate multi-agent debate with LLMs, show- ing that multiple model instances critiquing each other’s reasoning reduce hallucination and improve factual accu- racy. Khan et al. (2024) demonstrate that debate improves judge accuracy when debaters have access to information the judge lacks—an information asymmetry analogous to the LLM opponent surfacing inferential connections the re- spondent has not considered. Success is measured by bench- mark accuracy or complexity-theoretic expressiveness (Irv- ing, Christiano, and Amodei 2018). Elenchus shares with these systems the insight that ad- versarial structure can make unreliable AI outputs epistem- ically useful. The differences are structural. Debate frame- works are LLM-to-LLM systems aimed at answer quality; Elenchus is a human-AI system aimed at knowledge con- struction. In debate, the output is a consensus answer; in Elenchus, it is a structured consequence relation with full dialogical provenance. In debate, the human is a judge who selects between positions; in Elenchus, the human is the au- thor of the position, with authority over which inferences hold. 10 Limitations and future work 10.1 Automated reasoning over the logical extension to the material base Section 8 demonstrates integration with pyNMMS using the propositional fragment of the NMMS sequent calculus, ad- dressing the gap between material base construction and for- mal reasoning. Remaining work includes optimizing proof search for larger material bases (the current implementation uses exponential-time backward search with memoization) and integrating the reasoner into the Elenchus agent loop so that NMMS queries can inform the opponent’s challenge se- lection during the dialectic. 10.2 Propositional versus first-order logical vocabularies The base language L B S consists of atomic proposi- tional sentences introduced through dialogue.To allow the expression of quantified commitments like ”all birds fly”, an experimental extension to the pyNMMS package, pynmms.onto, provides seven defeasible ontology ax- iom schema types — subClassOf, range, domain, subProp- ertyOf, disjointWith, disjointProperties, and jointCommit- ment — that generate families of base axioms over concept and role assertions, evaluated lazily at query time. 5 This gives expressiveness comparable to RDFS 1.1 (Brickley and Guha 2014) — class hierarchies, property hierarchies, do- main and range constraints — augmented with material in- compatibility and joint inferential commitment, avoiding the need for a first-order extension to NMMS to support the ontological reasoning patterns most common in knowledge engineering. Modifying the Elenchus system prompt to al- low the respondent to make ontological commitments using these schema types, and to map the resulting dialectical state to an OntoMaterialBase, is future work. 10.3 Systematic oracle bias The LLM-as-oracle design handles false positives through contestation: incorrectly proposed tensions are rejected by 5 https://w.bradleypallen.org/pyNMMS/theory/ onto-extension/ the respondent. However, the protocol does not address false negatives—inferential relationships the LLM fails to surface because they fall outside its training distribution or reason- ing capabilities. The resulting material base may have sys- tematic lacunae invisible to both the respondent (who was never prompted to consider them) and the opponent (which cannot identify what it cannot identify). Future work will address mitigating this limitation. 10.4 Scalability The current case study operates over a single section of a specification. Scaling to larger domains will require manag- ing respondent cognitive load and LLM context limitations across longer dialectics. However, the GitHub-backed ar- chitecture already supports asynchronous, multi-session in- teraction, and the modular structure of the dialectical state — where each tension is independently resolvable — sug- gests that the protocol can decompose naturally along do- main boundaries. 10.5 Evaluation The case study presented here is illustrative rather than evaluative; it is an existence proof that the approach can work end-to-end in the context of an ontology engineer- ing task. The comparison validates the protocol’s cover- age and provides evidence that the protocol produces well- structured output aligned with independently documented design decisions, but does not provide evidence of discovery or epistemic novelty. A rigorous evaluation of the approach would require comparison with alternative knowledge ac- quisition methods on the same domain, assessment of inter- respondent consistency (do different experts produce com- parable material bases for the same domain?), and measure- ment of the coverage of the resulting knowledge base against gold-standard formalizations. We leave such evaluation to future work while noting that the traceability of Elenchus outputs (Section 4.3) facilitates such studies: every atomic proposition and material implication can be traced to a spe- cific dialogue move. 11 Conclusion We have presented Elenchus, a bilateral dialectical proto- col for generating knowledge bases from prover-skeptic di- alogues. Our main result is that Elenchus dialectical states map to material bases satisfying Containment—knowledge bases in the inferentialist sense—which can be further en- riched with logical vocabulary via NMMS. The knowledge base is fully traceable: every material implication originates in a specific dialogue move. Using pyNMMS, we have ver- ified that the material base produced by a single dialogue session over a PROV-O specification exhibits the structural properties predicted by the theory—nontransitivity, non- monotonicity, supraclassicality, conservativity—and that these properties correspond to specific design rationales doc- umented independently in Moreau et al. (2015). All cross- chain design resolutions are pairwise independent, confirm- ing that the Elenchus dialectic identified genuinely dis- tinct design tensions. The approach re-conceives knowl- edge engineering as dialogical explicitation of expert prac- tice, rather than extraction of pre-formed content. The LLM opponent serves as a defeasible derivability oracle, surfac- ing candidate tensions while the human respondent retains authority over which inferences hold. The structure of the mapping itself exhibits the explicitation pattern central to the inferentialist program: the two components of the base consequence relation make explicit, respectively, what the dialogue produced and what it presupposed. Future work will explore the use of the ontology engineering extensions to pyNMMS and the integration of the pyNMMS reasoner into the Elenchus agent loop, toward the goal of an end-to- end inferentialist knowledge engineering framework. Acknowledgments The author wishes to thank Robert Brandom, Kris Brown, Thomas Ferguson, Paul Groth, Ulf Hlobil, Filip Ilievski, Teresa Kouri Kissel, Shay Logan, Marcus Rossberg, and members of the Research Group On Logical Expressivism (ROLE) for their comments and feedback. References Allen, B. P., and Groth, P. 2025a. Evaluating Class Member- ship Relations in Knowledge Graphs using Large Language Models.In Mero ̃ no-Pe ̃ nuela, A.; ́ Oscar Corcho; Groth, P.; Simperl, E.; Tamma, V.; Nuzzolese, A. G.; Poveda- Villal ́ on, M.; Sabou, M.; Presutti, V.; Celino, I.; Revenko, A.; Raad, J.; Sartini, B.; and Lisena, P., eds., The Semantic Web: ESWC 2024 Satellite Events, volume 15344 of Lecture Notes in Computer Science. Cham: Springer. Allen, B. P., and Groth, P. T. 2025b. A Benchmark for the Detection of Metalinguistic Disagreements between LLMs and Knowledge Graphs. In Proceedings of the Special Ses- sion on Harmonising Generative AI and Semantic Web Tech- nologies (HGAIS 2024) co-located with the 23rd Interna- tional Semantic Web Conference (ISWC 2024), volume 3953 of CEUR Workshop Proceedings.Baltimore, Maryland: CEUR-WS.org. Allen, B. P.; Chhikara, P.; Ferguson, T. M.; Ilievski, F.; and Groth, P. 2025. Sound and Complete Neurosymbolic Rea- soning with LLM-Grounded Interpretations. In H. Gilpin, L.; Giunchiglia, E.; Hitzler, P.; and van Krieken, E., eds., Proceedings of The 19th International Conference on Neu- rosymbolic Learning and Reasoning, volume 284 of Pro- ceedings of Machine Learning Research, 392–419. PMLR. Allen, B. P. 2025a. Conceptual Engineering Using Large Language Models. In Vincent C. M ̈ uller, Leonard Dung, G. L., and Rumana, A., eds., Philosophy of Artificial Intelli- gence: The State of the Art). Springer Nature. To appear. Allen, B. P. 2025b. Elenchus: Dialectical Opponent for Research. GitHub repository. Allen, B. P. 2026. pyNMMS. PyPI package. Anthropic. 2025. Claude Code Overview. URL accessed: 2025-10-14. Babaei Giglou, H.; D’Souza, J.; and Auer, S.2023. LLMs4OL: Large language models for ontology learning. In Proceedings of the International Semantic Web Confer- ence. Belnap, N. 1977. How a computer should think. In Ryle, G., ed., Contemporary aspects of philosophy. Oriel Press. 30–55. Boose, J. H. 1985. A knowledge acquisition program for ex- pert systems based on personal construct psychology. Inter- national Journal of Man-Machine Studies 23(5):495–525. Brandom, R. 1994. Making it explicit: Reasoning, rep- resenting, and discursive commitment. Harvard University Press. Brickley, D., and Guha, R. 2014. RDF Schema 1.1. W3C recommendation, W3C. URL accessed: 2025-02-26. Cayrol, C., and Lagasquie-Schiex, M.-C. 2005. On the acceptability of arguments in bipolar argumentation frame- works. In Proceedings of the 8th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, 378–389. Cimiano, P. 2006. Ontology Learning and Population from Text: Algorithms, Evaluation and Applications. Springer. Ciroku, F.; de Berardinis, J.; Kim, J.; Mero ̃ no-Pe ̃ nuela, A.; Presutti, V.; and Simperl, E. 2024. Revont: Reverse en- gineering of competency questions from knowledge graphs via language models. Journal of Web Semantics 82:100822. Clark, P., and Porter, B. 1997. Building concept represen- tations from reusable components. In Proceedings of the fourteenth national conference on artificial intelligence and ninth conference on Innovative applications of artificial in- telligence, 369–376. Clark, P.; Thompson, J.; Barker, K.; Porter, B.; Chaudhri, V.; Rodriguez, A.; Thomere, J.; Mishra, S.; Gil, Y.; Hayes, P.; et al. 2001. Knowledge entry as the graphical assem- bly of components. In Proceedings of the 1st International Conference on Knowledge Capture, 22–29. del Carmen Su ́ arez de Figueroa Baonza, M. 2010. NeOn Methodology for Building Ontology Networks: Specifica- tion, Scheduling and Reuse. Ph.D. Dissertation, Universidad Polit ́ ecnica de Madrid, Madrid, Spain. Dung, P. M.1995.On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence 77(2):321–357. Dutilh Novaes, C. 2012. Formal languages in logic: A philosophical and cognitive analysis. Cambridge University Press. Dutilh Novaes, C. 2020. The dialogical roots of deduction: Historical, cognitive, and philosophical perspectives on rea- soning. Cambridge University Press. Dutilh Novaes, C. 2025. Proofs as Dialogues: The Enduring Significance of Lakatos for the Philosophy of Mathematical Practice. In Proofs and Research Programmes: Lakatos at 100. Springer. 27–46. Ericsson, K. A., and Simon, H. A. 1984. Protocol Analysis: Verbal Reports as Data. MIT Press. Feigenbaum, E. A. 1977. The art of artificial intelligence: Themes and case studies of knowledge engineering. In Pro- ceedings of the Fifth International Joint Conference on Ar- tificial Intelligence, volume 2. Boston. Fern ́ andez-L ́ opez, M.; G ́ omez-P ́ erez, A.; and Juristo, N. 1997. Methontology: From ontological art towards onto- logical engineering. In Proceedings of the AAAI-97 Spring Symposium Series on Ontological Engineering, 33–40. Forsythe, D. E. 1993. Engineering knowledge: The con- struction of knowledge in artificial intelligence. Social stud- ies of science 23(3):445–477. Garijo, D.; Poveda-Villal ́ on, M.; Amador-Dom ́ ınguez, E.; Wang, Z.; Garc ́ ıa-Castro, R.; and Corcho, O. 2024. Llms for ontology engineering: a landscape of tasks and bench- marking challenges. In The Semantic Web-ISWC. GitHub. 2025. About issues. URL accessed: 2025-02-01. Governatori, G.; Maher, M. J.; Antoniou, G.; and Billington, D. 2004. Argumentation semantics for defeasible logic. Journal of Logic and Computation 14(5):675–702. Gr ̈ uninger, M., and Fox, M. S. 1995. The role of compe- tency questions in enterprise engineering. In Benchmark- ing—Theory and practice. Springer. 22–31. Hlobil, U., and Brandom, R. B. 2025. Reasons for logic, logic for reasons: Pragmatics, semantics, and conceptual roles. Routledge. Irving, G.; Christiano, P.; and Amodei, D. 2018. Ai safety via debate. arXiv preprint arXiv:1805.00899. Kampars, J.; Mosans, G.; Jogi, T.; Roters, F.; and Va- jragupta, N. 2025. Llm-supported collaborative ontology de- sign for data and knowledge management platforms. Fron- tiers in big Data 8:1676477. Khan, A.; Hughes, J.; Valentine, D.; Ruis, L.; Sachan, K.; Radhakrishnan, A.; Grefenstette, E.; Bowman, S. R.; Rockt ̈ aschel, T.; and Perez, E.2024.Debating with more persuasive llms leads to more truthful answers. arXiv preprint arXiv:2402.06782. Koutsiana, E.; Walker, J.; Nwachukwu, M.; Mero ̃ no- Pe ̃ nuela, A.; and Simperl, E. 2024. Knowledge Prompting: How Knowledge Engineers Use Large Language Models. arXiv preprint arXiv:2408.08878. Lebo, T.; Sahoo, S.; and McGuinness, D. 2013. PROV- O: The PROV Ontology.W3c recommendation, W3C. https://w.w3.org/TR/prov-o/. Li, Y.; Du, Y.; Zhang, J.; Hou, L.; Grabowski, P.; Li, Y.; and Ie, E. 2024. Improving multi-agent debate with sparse communication topology. arXiv preprint arXiv:2406.11776. Liang, T.; He, Z.; Jiao, W.; Wang, X.; Wang, Y.; Wang, R.; Yang, Y.; Shi, S.; and Tu, Z. 2024. Encouraging divergent thinking in large language models through multi-agent de- bate. In Proceedings of the 2024 conference on empirical methods in natural language processing, 17889–17904. Lorenzen, P., and Lorenz, K. 1978. Dialogische Logik. Wis- senschaftliche Buchgesellschaft. Modgil, S., and Prakken, H. 2014. The ASPIC+ frame- work for structured argumentation: A tutorial. Argument & Computation 5(1):31–62. Moreau, L.; Groth, P.; Cheney, J.; Lebo, T.; and Miles, S. 2015. The rationale of PROV. Journal of Web Semantics 35:235–257. Prakken, H. 2006. Formal systems for persuasion dialogue. The Knowledge Engineering Review 21(2):163–188. Restall, G. 2005. Multiple conclusions. In Logic, method- ology and philosophy of science: Proceedings of the twelfth international congress, 189–205. Kings College Publica- tions. Schreiber, A. T.; Schreiber, G.; Akkermans, H.; Anjewier- den, A.; Shadbolt, N.; de Hoog, R.; Van de Velde, W.; and Wielinga, B. 2000. Knowledge engineering and manage- ment: the CommonKADS methodology. MIT Press. Sellars, W.1953.Inference and meaning.Mind 62(247):313–338. Studer, R.; Benjamins, V. R.; and Fensel, D. 1998. Knowl- edge engineering: Principles and methods. Data & knowl- edge engineering 25(1-2):161–197. Wei, X.; Cui, X.; Cheng, N.; Wang, X.; Zhang, X.; Huang, S.; Xie, P.; Xu, J.; Chen, Y.; Zhang, M.; et al. 2023. Chatie: Zero-shot Information Extraction via Chatting with Chat- GPT. arXiv preprint arXiv:2302.10205. Yao, L.; Peng, J.; Mao, C.; and Luo, Y. 2025. Explor- ing large language models for knowledge graph comple- tion. In ICASSP 2025-2025 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), 1–5. IEEE. Zhang, B.; Carriero, V. A.; Schreiberhuber, K.; Tsaneva, S.; Gonz ́ alez, L. S.; Kim, J.; and de Berardinis, J. 2024. On- tochat: a framework for conversational ontology engineer- ing using language models. In European Semantic Web Con- ference, 102–121. Springer. Zhao, Y.; Zhang, B.; Hu, X.; Ouyang, S.; Kim, J.; Jain, N.; De Berardinis, J.; Mero ̃ no-Pe ̃ nuela, A.; and Simperl, E. 2024. Improving ontology requirements engineering with ontochat and participatory prompting. In Proceedings of the AAAI Symposium Series, volume 4:1, 253–257.