transhumanist_atom_understander's Shortform

This is a special post for quick takes by transhumanist_atom_understander. Only they can create top-level comments. Comments here also appear on the Quick Takes page and All Posts page.

Does anyone have software they like for doing provability logic? Two use cases:

Deciding theorems of GL. I recently made a post which had two derivations in GL. GL is decidable, so I should be able to write them as material implications and run some program to check if they're theorems. I have no idea what program people would actually use for this though.
Computing fixed points. For that post, I would want to input the "equation" , and get as output the "solution" for , which is . That's all you need for a much shorter proof than the one I did. Does the MIRI provability repo do this somehow? Or is there some standard tool?

Does anyone have software they like for doing provability logic? Two use cases:

Deciding theorems of GL. I recently made a post which had two derivations in GL. GL is decidable, so I should be able to write them as material implications and run some program to check if they're theorems. I have no idea what program people would actually use for this though.
Computing fixed points. For that post, I would want to input the "equation" , and get as output the "solution" for , which is . That's all you need for a much shorter proof than the one I did. Does the MIRI provability repo do this somehow? Or is there some standard tool?

5