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

Sep 26, 2026

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

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.

Jorryt de Jong, Stefan Moraca, Ettore Cesari +1

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

LLM Reasoning Natural Language Inference Logical Reasoning

Ask PDF

Aug 7, 2026

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

We present a web demo for exploring a large-scale disambiguated knowledge base (KB) materialized from a large language model (LLM). GPTKB 2.0 contains 38.4M triples over 1.6M canonical entities, together with 207.6K consolidated relations and 66K consolidated classes. Unlike prior LLM-derived knowledge bases that largely identify entities by surface strings, GPTKB 2.0 performs context-guided disambiguation during recursive KB construction, separating homonyms and merging synonymous mentions as facts are elicited. The demo makes this process inspectable: users can browse entities, follow links across the KB, and audit the provenance of individual facts, including surface forms, candidate matches, source triples, and disambiguation decisions. The interface further supports structured SPARQL queries, natural-language questions translated to SPARQL, and entity linking from user-provided text to canonical GPTKB 2.0 entries. GPTKB 2.0 is available at https://gptkb.org/, with the full KB downloadable for offline use.

Yujia Hu, Tuan-Phong Nguyen, Simon Razniewski

ScaDS.AI Dresden/Leipzig & TU Dresden, Germany · VNU University of Engineering and Technology, Hanoi, Vietnam

KG Construction Entity Resolution LLM Information Extraction Knowledge Graphs

Ask PDF

Jul 8, 2025

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

Language models are powerful artifacts, yet their factual knowledge is still poorly understood, and inaccessible to ad-hoc browsing and scalable statistical analysis. This demonstration introduces GPTKB v1.5, a densely interlinked 100-million-triple knowledge base (KB) built for $14,000 from GPT-4.1, using the GPTKB methodology for massive-recursive LLM knowledge materialization. This demo focuses on three use cases: (1) link-traversal-based LLM knowledge exploration, (2) SPARQL-based structured LLM knowledge querying, (3) comparative exploration of the strengths and weaknesses of LLM knowledge. Massive-recursive LLM knowledge materialization is a groundbreaking opportunity both for the systematic analysis of LLM knowledge, as well as for automated KB construction.

Yujia Hu, Tuan-Phong Nguyen, Shrestha Ghosh +2

ScaDS.AI Dresden/Leipzig & TU Dresden, Germany · VNU University of Engineering and Technology, Hanoi, Vietnam · University of Tübingen, Germany

KG Construction LLM Information Extraction Factual Knowledge in Language Models Knowledge Graphs

Ask PDF