# Isabelle Formalisation of Original Representation Theorems

arXiv: https://arxiv.org/abs/2306.10558 · HTML: https://mlsanity.com/paper/2306.10558/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 23 references that are in the map.
- First posted on arXiv 18 Jun 2023.

## Builds on (most cited first, 3 of 3)

- [Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?](https://mlsanity.com/paper/1406.0774/) (2014)
- [A Verified Algorithm Enumerating Event Structures](https://mlsanity.com/paper/1705.07228/) (2017)
- [Representation Theorems Obtained by Miningacross Web Sources for Hints](https://mlsanity.com/paper/2306.00584/) (2023)

## Abstract (arXiv)

In a recent paper, new theorems linking apparently unrelated mathematical objects (event structures from concurrency theory and full graphs arising in computational biology) were discovered by cross-site data mining on huge databases, and building on existing Isabelle-verified event structures enumeration algorithms. Given the origin and newness of such theorems, their formal verification is particularly desirable. This paper presents such a verification via Isabelle/HOL definitions and theorems, and exposes the technical challenges found in the process. The introduced formalisation completes the verification of Isabelle-verified event structure enumeration algorithms into a fully verified framework to link event structures to full graphs.