Projects per year
Abstract
An event structure is a mathematical abstraction modeling concepts as causality, conflict and concurrency between events. While many other mathematical structures, including groups, topological spaces, rings, abound with algorithms and formulas to generate, enumerate and count particular sets of their members, no algorithm or formulas are known to generate or count all the possible event structures over af inite set of events. We present an algorithm to generate such a family, along with a functional implementation verified using Isabelle/HOL. As byproducts, we obtain a verified enumeration of all possible preorders and partial orders. While the integer sequences counting preorders and partial orders are already listed on OEIS (Online Encyclopedia of Integer Sequences), the one counting event structures is not. We therefore used our algorithm to submit a formally verified addition, which has been successfully reviewed and is now part of the OEIS.
Original language  English 

Title of host publication  Intelligent Computer Mathematics 
Subtitle of host publication  10th International Conference, CICM 2017, Edinburgh, UK, July 1721, 2017, Proceedings 
Editors  Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, Olaf Teschke 
Place of Publication  Cham 
Publisher  Springer 
Pages  239254 
ISBN (Print)  9783319620749, 9783319620756 
DOIs  
Publication status  Published  2017 
Event  10th Conference on Intelligent Computer Mathematics (CICM 2017)  Edinburgh, United Kingdom Duration: 17 Jul 2017 → 21 Jul 2017 Conference number: 10 http://www.cicmconference.org/2017 
Publication series
Name  Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence) 

Publisher  Springer 
Volume  10383 
ISSN (Print)  03029743 
Conference
Conference  10th Conference on Intelligent Computer Mathematics (CICM 2017) 

Abbreviated title  CICM 
Country/Territory  United Kingdom 
City  Edinburgh 
Period  17/07/17 → 21/07/17 
Internet address 
Fingerprint
Dive into the research topics of 'A verified algorithm enumerating event structures'. Together they form a unique fingerprint.Projects
 1 Finished

Automated Conflict Resolution: Automated Conflic Resolution in Clinical Pathways
1/07/15 → 15/12/18
Project: Standard
Profiles
Datasets

A verified algorithm enumerating event structures (dataset)
Kuster Filipe Bowles, J. (Creator) & Caminati, M. B. (Creator), Bitbucket, 2017
https://bitbucket.org/caminati/oeises
Dataset