diff --git a/web/authors/hofmeier/index.html b/web/authors/hofmeier/index.html new file mode 100644 --- /dev/null +++ b/web/authors/hofmeier/index.html @@ -0,0 +1,99 @@ + + + + + + Paul Hofmeier- Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Paul Hofmeier

+
+ + + +
+
+ +

E-Mails 📧

+ + + +

Entries

2022

+ + + + +
+
+ + + \ No newline at end of file diff --git a/web/authors/hofmeier/index.xml b/web/authors/hofmeier/index.xml new file mode 100644 --- /dev/null +++ b/web/authors/hofmeier/index.xml @@ -0,0 +1,20 @@ + + + + hofmeier on Archive of Formal Proofs + /authors/hofmeier/ + Recent content in hofmeier on Archive of Formal Proofs + Hugo -- gohugo.io + en-gb + Fri, 11 Nov 2022 00:00:00 +0000 + + Combinatorial Enumeration Algorithms + /entries/Combinatorial_Enumeration_Algorithms.html + Fri, 11 Nov 2022 00:00:00 +0000 + + /entries/Combinatorial_Enumeration_Algorithms.html + + + + + diff --git a/web/dependencies/falling_factorial_sum/index.html b/web/dependencies/falling_factorial_sum/index.html new file mode 100644 --- /dev/null +++ b/web/dependencies/falling_factorial_sum/index.html @@ -0,0 +1,92 @@ + + + + + + Falling_Factorial_Sum - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Falling_Factorial_Sum Dependents

+
+ + +
+

2022

+ + + + +
+
+ + + \ No newline at end of file diff --git a/web/dependencies/falling_factorial_sum/index.xml b/web/dependencies/falling_factorial_sum/index.xml new file mode 100644 --- /dev/null +++ b/web/dependencies/falling_factorial_sum/index.xml @@ -0,0 +1,20 @@ + + + + Falling_Factorial_Sum on Archive of Formal Proofs + /dependencies/falling_factorial_sum/ + Recent content in Falling_Factorial_Sum on Archive of Formal Proofs + Hugo -- gohugo.io + en-gb + Fri, 11 Nov 2022 00:00:00 +0000 + + Combinatorial Enumeration Algorithms + /entries/Combinatorial_Enumeration_Algorithms.html + Fri, 11 Nov 2022 00:00:00 +0000 + + /entries/Combinatorial_Enumeration_Algorithms.html + + + + + diff --git a/web/entries/Combinatorial_Enumeration_Algorithms.html b/web/entries/Combinatorial_Enumeration_Algorithms.html new file mode 100644 --- /dev/null +++ b/web/entries/Combinatorial_Enumeration_Algorithms.html @@ -0,0 +1,185 @@ + + + + + + Combinatorial Enumeration Algorithms - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Combinatorial Enumeration Algorithms

+
+ +

Paul Hofmeier 📧 and Emin Karayel 📧 +

+ + +

November 11, 2022

+ +
+

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

+ +

Session Combinatorial_Enumeration_Algorithms

+
+
+

Depends on

+ +
+ +
+

Auto-related entries

+ +
+ +
+
+ + + +
+ +
+

Cite

+ × +
+ 
@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 + +
+
+
+
+ + + \ No newline at end of file diff --git a/web/theories/combinatorial_enumeration_algorithms/index.html b/web/theories/combinatorial_enumeration_algorithms/index.html new file mode 100644 --- /dev/null +++ b/web/theories/combinatorial_enumeration_algorithms/index.html @@ -0,0 +1,94 @@ + + + + + + Combinatorial_Enumeration_Algorithms - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ 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

+
+
+ + + \ No newline at end of file