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.9.tar.gz
sha512=d793c993b50dd1149475ed7131ddb7910a30b6711c97f3ae8079661e2e8f4211ce8b4d85ade9e57c176b05feb20edb59d286db883a5873e3c775aac0fb1e40c5

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-05-20

Published: 25 May 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.6"
  2. coq-goedel >= "8.13.0"

Conflicts

None