Isabelle Formalisation of Original Representation Theorems
This work provides formal verification for cross-disciplinary mathematical theorems, which is incremental as it builds on existing Isabelle-verified algorithms.
The paper tackles the formal verification of newly discovered theorems linking event structures from concurrency theory and full graphs from computational biology, using Isabelle/HOL to complete a fully verified framework.
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.