### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Combinatorics
- Computer science/Algorithms

### Related publications

- Hofmeier, Paul. (2022). Verification of Combinatorial Algorithms [Bachelor's Thesis, Technische Universität München]. mediaTUM. https://mediatum.ub.tum.de/1693026

### Session Combinatorial_Enumeration_Algorithms

- Common_Lemmas
- n_Sequences
- n_Permutations
- Filter_Bool_List
- n_Subsets
- Powerset
- Integer_Partitions
- Integer_Compositions
- Weak_Integer_Compositions
- Derangements_Enum
- Trees
- Combinatorial_Enumeration_Algorithms

### Depends on

- Cardinality of Number Partitions
- The Falling Factorial of a Sum

### Auto-related entries

- Verifying Imperative Programs using Auto2
- Hoare Logics for Time Bounds
- COMPLX: A Verification Framework for Concurrent Imperative Programs
- Algebraic Numbers in Isabelle/HOL
- A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment

## Cite

×

Combinatorial_Enumeration_Algorithms-AFP

    @article{Combinatorial_Enumeration_Algorithms-AFP,
      author  = {Paul Hofmeier and Emin Karayel},
      title   = {Combinatorial Enumeration Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Combinatorial_Enumeration_Algorithms.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Nov 14, 2022 : Isabelle2022