Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

Bradley P. Allen

cs.CLMar 7, 2026

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

Authors: Bradley P. Allen

Organizations: University of Amsterdam

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.

Figures & tables

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 7 .

Figure 3: A GitHub issue capturing a challenge made by the LLM opponent in the course of an Elenchus dialectic described in Section 7 .

Issue #	Commitment	Proposition
1	Three core classes form the basis of PROV-O: Entity, Activity, Agent	$p_{1}$
2	Entity is a thing with fixed aspects	$p_{2}$
3	Activity is something that occurs over time and acts upon or with entities	$p_{3}$
4	Agent bears responsibility for activities, entities, or other agents’ activities	$p_{4}$
5	used and wasGeneratedBy relate Activities to Entities	$p_{5}$
6	wasInformedBy provides Activity-to-Activity dependency	$p_{6}$

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	[ 35 ]	Resolution	Proposition	Material Implication
11	Fixed aspects; entity change?	RE1, RE3, RE5, RE6, EZ1	Pragmatist: context-relative individuation	$p_{18}$	$p_{2}\mathrel{\mid\!\sim}p_{18}$
12	Activity duration; instants?	EV1, EV4	Durational activities; instantaneous events	$p_{27}$	$p_{3}\mathrel{\mid\!\sim}p_{27}$
13	Responsibility vs. causation?	XG5, VI2–4, GE1	Agency is pragmatic ascription	$p_{29}$	$p_{4}\mathrel{\mid\!\sim}p_{29}$
14	wasInformedBy : shortcut?	VI1, VI6, EZ1	Independent: inferred, not reducible	$p_{30}$	$p_{6}\mathrel{\mid\!\sim}p_{30}$
15	Derivation criteria; identity?	XG8, VI5, VI6	Broad causal dependencies; subtypes narrow	$p_{28}$	$p_{7}\mathrel{\mid\!\sim}p_{28}$
16	Delegation responsibility?	XG11 (partial)	Hierarchical and transitive	$p_{25},p_{26}$	$p_{9}\mathrel{\mid\!\sim}p_{25}$ , $p_{9}\mathrel{\mid\!\sim}p_{26}$

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

Base consequences (all 9 derivable)
Query	Result
$p_{2}\mathrel{\mid\!\sim}p_{18}$ , $p_{3}\mathrel{\mid\!\sim}p_{27}$ , $p_{4}\mathrel{\mid\!\sim}p_{29}$ , $p_{6}\mathrel{\mid\!\sim}p_{30}$	True
$p_{7}\mathrel{\mid\!\sim}p_{28}$ , $p_{9}\mathrel{\mid\!\sim}p_{25}$ , $p_{9}\mathrel{\mid\!\sim}p_{26}$ , $p_{10}\mathrel{\mid\!\sim}p_{24}$ , $p_{18}\mathrel{\mid\!\sim}p_{23}$	True
Nontransitivity
$p_{2}\mathrel{\mid\!\sim}p_{18}$ and $p_{18}\mathrel{\mid\!\sim}p_{23}$	True
$p_{2}\mathrel{\mid\!\sim}p_{23}$	False

Table 3: Structural properties of the PROV-O material base verified 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 supraclassical and conservative.

Requirement	Query	Result	Property
EZ3	$p_{2}\mathrel{\mid\!\sim}p_{23}$	F	Nontrans.
EZ3	$\mathrel{\mid\!\sim}(p_{2}{\to}p_{18}){\land}(p_{18}{\to}p_{23}){\to}(p_{2}{\to}p_{23})$	T	Supraclass.
EZ3	$\mathrel{\mid\!\sim}p_{2}\to p_{23}$	F	Nontrans.
VI5	$p_{7}\mathrel{\mid\!\sim}p_{28}$	T	Base
VI5	$p_{28}\mathrel{\mid\!\sim}p_{7}$	F	Directional
VI1	$p_{2}\mathrel{\mid\!\sim}p_{27}$ , $p_{2}\mathrel{\mid\!\sim}p_{29}$	F	Indep.

Table 4: Design rationale queries mapping NMMS reasoning results to requirements documented in Moreau et al. ( ? ). 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).

Explore similar work

Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs
Sep 26, 2026Jorryt de Jong, Stefan Moraca, Ettore Cesari +1LLM Reasoning Natural Language Inference
Utrecht University, the Netherlands · Institute for Language Sciences, Utrecht University, the Netherlands
GPTKB 2.0: Browsing, Querying, and Auditing a Disambiguated LLM-Derived Knowledge Base
Aug 7, 2026Yujia Hu, Tuan-Phong Nguyen, Simon RazniewskiKG Construction Entity Resolution
ScaDS.AI Dresden/Leipzig & TU Dresden, Germany · VNU University of Engineering and Technology, Hanoi, Vietnam
GPTKB v1.5: A Massive Knowledge Base for Exploring Factual LLM Knowledge
Jul 8, 2025Yujia Hu, Tuan-Phong Nguyen, Shrestha Ghosh +2KG Construction LLM Information Extraction
ScaDS.AI Dresden/Leipzig & TU Dresden, Germany · VNU University of Engineering and Technology, Hanoi, Vietnam · University of Tübingen, Germany

Sep 26, 2026J/K move · Enter open · S save

Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs

Jorryt de Jong, Stefan Moraca, Ettore Cesari, Lasha Abzianidze

Utrecht University, the Netherlands · Institute for Language Sciences, Utrecht University, the Netherlands

LLM Reasoning Natural Language Inference Logical Reasoning

Open paper AskPDF arXiv

Large Language Models (LLMs) are highly capable of natural language reasoning and appear to store a great deal of lexical knowledge, but it is still unclear how much of this knowledge they actually use when reasoning, and whether they use it in the right way. On the other hand, logic-based Natural Language Inference (NLI) systems provide transparent and formally grounded reasoning, but they need to be supplied with rich lexical knowledge to prove inferences beyond purely logical ones. In this paper, we evaluate whether LLMs can identify all lexical knowledge needed to solve NLI problems and how much this knowledge contributes to proof search in a logic-based NLI system. Our research focuses exclusively on structured lexical entailments (e.g., chinchilla

\sqsubseteq

small animal) as a proxy for structured explanations for NLI problems with an entailment label. First, we curate a dataset for a new task of explaining sentential entailments with a set of lexical entailments. The dataset is used to intrinsically evaluate LLMs on generating structured lexical explanations. Then, we use NLI as an extrinsic evaluation in a simple neuro-symbolic setting, assessing whether LLMs can supply sufficient lexical relations to LangPro, a natural-logic theorem prover for natural language. The results show that the proposed task remains challenging even for hosted proprietary LLMs, and that their contribution to theorem proving is moderate: generated relations are often only partially sound and may be tailored to the specific NLI problem rather than representing generally valid lexical knowledge.

Abstract

Explore similar work

Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs

GPTKB 2.0: Browsing, Querying, and Auditing a Disambiguated LLM-Derived Knowledge Base

GPTKB v1.5: A Massive Knowledge Base for Exploring Factual LLM Knowledge