Isabelle Formalisation of Original Representation Theorems

Marco B. Caminati
6/18/2023
cs.LOcs.AI

No confident code implementation found for this paper.

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Cite this paper

@article{caminati2023isabelle,
  title  = {Isabelle Formalisation of Original Representation Theorems},
  author = {Marco B. Caminati},
  year   = {2023},
  eprint = {2306.10558},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2306.10558v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2306.10558.svg)](https://codeofpaper.com/paper/2306.10558)

Discussion