Commenting specifically to call out other decider authors whose work was used in the CTL library construction: @Iijil (GitHub - Iijil1/Bruteforce-CTL: An attempt to proof that a turing machine doesn't halt by finding a closed tape language using bruteforce), @Nathan-Fenner (GitHub - Nathan-Fenner/bb-simple-n-gram-cps), @TonyG (bbchallenge/Bouncers at main · TonyGuil/bbchallenge · GitHub), savask (The closed position set decider, reverse-engineered from Skelet's program · GitHub).
Update: Skelet too, now.
Indirectly, also @Frans_Faase (GitHub - FransFaase/SymbolicTM: Symbolic Turing Machine for Busy Beaver problems).
You are coauthors of this proof library.
I plan to release polished conversion utilities at some point, at least for most of these. (n-gram CPS has to be modified before it can emit convertible proof data – but the conversion is very smooth after that.)
1 Like