A verified algorithm enumerating event structures
From MaRDI portal
Publication:2364684
DOI10.1007/978-3-319-62075-6_17zbMath1367.68245arXiv1705.07228MaRDI QIDQ2364684
Marco Bright Caminati, Juliana Küster-Filipe
Publication date: 21 July 2017
Full work available at URL: https://arxiv.org/abs/1705.07228
automated reasoning; enumeration; counting; formal methods; logic; discrete; event structures; Isabelle/HOL; verified algorithm; OEIS
05A15: Exact enumeration problems, generating functions
68Q10: Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68U35: Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
06-04: Software, source code, etc. for problems pertaining to ordered structures
Related Items
Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation, Isabelle formalisation of original representation theorems, Tests and proofs for custom data generators
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Finite labelling problem in event structures
- Conjugacy classes in unitriangular matrices.
- Contextual Petri nets, asymmetric event structures, and processes
- Mechanical Analysis of Finite Idempotent Relations
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Formal Proof of SCHUR Conjugate Function
- Decomposing Interactions
- Asymptotic Enumeration of Partial Orders on a Finite Set
- Enumeration of AG-Groupoids
- The Transitive Reduction of a Directed Graph
- Event Structure Semantics for Nominal Calculi