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.5.tar.gz
sha512=7edd74fa408b996ebe7c4748046fda522f24a4b532c58b5ad55edeaa4bbd137ba9f21b0b6c1f824d4e7c50f04fb6afe488dfbcd24702e8fe44eb75b780610458

Description

An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant. This development 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:2021-10-15

Published: 15 Oct 2021

Dependencies (3)

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

Dev Dependencies

None

Used by (2)

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

Conflicts

None