原有表征定理的Isabelle形式化

Jun, 2023

Isabelle Formalisation of Original Representation Theorems

Marco B. Caminati

TL;DR本篇论文基于Isabelle-verified事件结构枚举算法，通过对巨大数据库进行跨站数据挖掘，发现了连接看似不相关的数学对象（并发理论中的事件结构和计算生物学中的完整图）的新定理，并通过Isabelle/HOL定义和定理进行了形式验证，完成了Isabelle-verified事件结构枚举算法验证的全面验证框架以链接事件结构和完整图。

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 min