Isabelle Formalisation of Original Representation Theorems
Abstract
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.
Keywords
Cite
@article{arxiv.2306.10558,
title = {Isabelle Formalisation of Original Representation Theorems},
author = {Marco B. Caminati},
journal= {arXiv preprint arXiv:2306.10558},
year = {2023}
}
Comments
accepted by CICM 2023 conference (regular paper)