Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Combinatorial Enumeration Algo...


view this post on Zulip Email Gateway (Nov 14 2022 at 10:46):

From: Tobias Nipkow <nipkow@in.tum.de>
Combinatorial Enumeration Algorithms

Paul Hofmeier and Emin Karayel

Combinatorial objects have configurations which can be enumerated by algorithms,
but especially for imperative programs, it is difficult to find out if they
produce the correct output and don’t generate duplicates. Therefore, for some of
the most common combinatorial objects, namely n_Sequences, n_Permutations,
n_Subsets, Powerset, Integer_Compositions, Integer_Partitions,
Weak_Integer_Compositions, Derangements and Trees, this entry formalizes
efficient functional programs and verifies their correctness. In addition, it
provides cardinality proofs for those combinatorial objects. Some cardinalities
are verified using the enumeration functions and others are shown using existing
libraries including other AFP entries.

https://www.isa-afp.org/entries/Combinatorial_Enumeration_Algorithms.html

PS More such enumeration algorithms are welcome.
smime.p7s


Last updated: Mar 29 2024 at 12:28 UTC