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”