VLDB 2026 Research / reviewers in the wild / expert
Edvard K. Holden
dblp:297/5021
· DBLP profile ↗
2ranked-venue papers
2as first author
2since 2021 · last 2025
0000-0002-8782-3960ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 2 · 2 first-author · 2 since 2021Artificial intelligence and machine learning · 1 · 1 first-author · 1 since 2021Software engineering, systems software and programming languages · 1 · 1 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Graph sequence learning for premise selectionabstractPremise selection is crucial for large theory reasoning with automated theorem provers as the sheer size of the problems quickly leads to resource exhaustion. This paper proposes a premise selection method inspired by the machine learning domain of image captioning, where language models automatically generate a suitable caption for a given image. Likewise, we attempt to generate the sequence of axioms required to construct the proof of a given conjecture. In our axiom captioning approach, a pre-trained graph neural network is combined with a language model via transfer learning to encapsulate both the inter-axiom and conjecture-axiom relationships. We evaluate different configurations of our method and experience a 14% improvement in the number of solved problems over a baseline. Edvard K. Holden, Konstantin Korovin |
J. Symb. Comput. | 1 |
| 2021 | Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving
Edvard K. Holden, Konstantin Korovin |
CICM | 1 |