Isabelle formalisation of original representation theorems

DOI10.1007/978-3-031-42753-4_7MaRDI QIDQ6118819zbMATH OpenFDO

Authors Marco Caminati

Publication date 28 February 2024

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2306.10558

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

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.

Recommendations

• A verified algorithm enumerating event structures
• Verifying randomised social choice
• A graph library for Isabelle
• The Isabelle Framework
• On the role of formalization in computational mathematics

Cites work

• A graph library for Isabelle
• A verified algorithm enumerating event structures
• An example of formalizing recent mathematical results in MIZAR
• Asymptotic enumeration of full graphs
• Enumeration of Full Graphs: Onset of the Asymptotic Region
• Extending Sledgehammer with SMT solvers
• Handbook of Graph Theory
• scientific article; zbMATH DE number 3595177 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• Incidence matrices and interval graphs
• Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof pearl: a probabilistic proof for the girth-chromatic number theorem
• Some considerations on the usability of interactive provers
• The On-Line Encyclopedia of Integer Sequences

This page was built for publication: Isabelle formalisation of original representation theorems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6118819)