package coq-hydra-battles

  1. Overview
  2. No Docs
Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq

Install

Dune Dependency

github.com Edit opam file Versions (4)

Authors

  1. P
    Pierre Castéran
  2. Ã
    Évelyne Contejean
  3. J
    Jeremy Damour
  4. R
    Russell O'Connor
  5. K
    Karl Palmskog
  6. C
    Clément Pit-Claudel
  7. T
    Théo Zimmermann

Maintainers

  1. P
    palmskog@gmail.com

Sources

v0.6.tar.gz
sha512=a7e5e16506ad4eb2b5968d6bffbc1dacb297a304c7e8bbbd2ec4d2488d2090573288bdcd0e17fa05b605925b71c3ece5e46e91134d98f47248ef173c92dc8ed7

Description

An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq proof assistant. This includes the study of several representations of ordinal numbers, and a part of the so-called Ketonen and Solovay machinery (combinatorial properties of epsilon0).

Tags

category:Mathematics/Combinatorics and Graph Theory category:Mathematics/Logic/Foundations keyword:Ketonen-Solovay machinery keyword:ordinal numbers keyword:primitive recursive functions logpath:hydras date:2022-02-17

Published: 28 Feb 2022

Dependencies (4)

  1. coq-libhyps
  2. coq-equations >= "1.2" & < "1.4~"
  3. coq >= "8.13" & < "8.16~"
  4. dune >= "2.5"

Dev Dependencies

None

Used by (2)

  1. coq-gaia-hydras < "0.9"
  2. coq-goedel >= "8.13.0"

Conflicts

None