A verified algorithm enumerating event structures

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

zbMATH Keywords

automated reasoning; enumeration; counting; formal methods; logic; discrete; event structures; Isabelle/HOL; verified algorithm; OEIS

Mathematics Subject Classification ID

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

• Isabelle
• Isabelle/HOL
• HOL
• OEIS
• FinFuns

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