Isabelle Formalisation of Original Representation Theorems

Autor:	Caminati, Marco B.
Rok vydání:	2023
Předmět:	Computer Science - Logic in Computer Science Computer Science - Artificial Intelligence
Druh dokumentu:	Working Paper
Popis:	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. Comment: accepted by CICM 2023 conference (regular paper)
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2306.10558 Zobrazit plný text záznamu View this record from Arxiv