Tests and Proofs for Enumerative Combinatorics

DOI10.1007/978-3-319-41135-4_4MaRDI QIDQ2827441zbMATH OpenOpenAlexFDO

Authors Catherine Dubois, Alain Giorgetti, Richard Genestier

Publication date 19 October 2016

Published in Tests and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-41135-4_4

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to combinatorics (05-04) Enumerative combinatorics (05A99) Logic programming (68N17) Randomized algorithms (68W20)

Recommendations

• Combinatorial proofs of some enumeration identities
• scientific article; zbMATH DE number 1241385
• scientific article; zbMATH DE number 7307076
• On combinatorial testing problems
• scientific article; zbMATH DE number 3880787
• scientific article; zbMATH DE number 1774199
• scientific article; zbMATH DE number 2148993
• Overview of some general results in combinatorial enumeration
• Two Proofs in Combinatorial Number Theory

Cites work

• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Combinatorial Oriented Maps
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Foundational property-based testing
• Graphs on surfaces and their applications. Appendix by Don B. Zagier
• scientific article; zbMATH DE number 3407696 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Patterns in permutations and words.
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
• The Four Colour Theorem: Engineering of a Formal Proof
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof

Cited in

(5)

• Tests and proofs for custom data generators
• Study of the bounds on the number of basic sets in a test.
• Fair enumeration combinators
• On combinatorial testing problems
• On planarity of graphs in homotopy type theory

Describes a project that uses

Uses Software

• Coq
• Nitpick
• PVS
• Haskell
• FocalTest
• OEIS
• QuickCheck
• SmallCheck
• QuickChick
• Mathematical Components
• GitHub

This page was built for publication: Tests and Proofs for Enumerative Combinatorics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2827441)