.png){kind=icon}
.png){kind=icon}
Return
Certified Algorithms for Numerical Semigroups in Rocq
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-07021-0_19.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
A numerical semigroup is a co-finite submonoid of the monoid of non-negative integers under addition. Many properties of numerical semigroups rely on some fundamental invariants, such as, among others, the set of gaps (and its cardinality), the Apery set or the Frobenius number. Algorithms for calculating invariants are currently based on computational tools, such as GAP, which lack proofs (either formal or informal) of their correctness. In this paper we introduce a Rocq formalization of numerical semigroups. Given the semigroup generators, we provide certified algorithms for computing some of the fundamental invariants: the set of gaps, of small elements, the Apery set, the multiplicity, the conductor and the Frobenius number. To the best of our knowledge this is the first formalization of numerical semigroups in any proof assistant.
Keywords:
Numerical semigroups
Coq/Rocq
Verified theory formalization
Journal
I
IF:
0
Papers:
25
Citations:
0