Trying to implement logic as a game

I see!
Thank you very much, that sounds like great advice!
I will try to implement that as soon as I can

Managing assumptions/boxes can get a little tricky; the tree structure goes beyond the types of geometric relationships found in most board games. It's probably going to involve recursion in some sense.

One restriction is that a given sentence name (or function name) is supposed to have a consistent number of arguments. (This is inconsistently enforced, but breaking it would make it difficult to write rules involving it anyway.) Technically, I think you could get around this with a "linked list" approach like (known (assumptions foo (assumptions bar (assumptions baz null))) formula), but this is unwieldy and would break a lot of players.

So it's probably better to break the information about assumptions out into multiple sentence types (like having multiple tables in a database). It would help to have some kind of "key" to "join" these sentences together on, to continue the database analogy. It might work if the key referred to the formula, but it would probably be easier to have it refer to the box (or set of assumptions).

So then you'd have something like (true (known box4 p)) along with (true (assumption box4 q)), (true (known box4 q)), and (true (boxIsInside box4 box2)). Say you also have (true (boxIsInside box2 box1)) and box1 is the starting point. (The proof isn't over until you've achieved (true (known box1 whateverYouWantToProve)).)

I assume the progress of the game from step-to-step is going down the list of statements in the proof, so we also have a box we're currently in, (true (currentBox box4)); and that would also handle the problem of how to exclude statements from box2 that occur after box4 is closed.

So then the statements we can access are those whose boxes we are in, which we can find with the help of recursion:
(<= (accessible ?statement)
(accessibleBox ?box)
(true (known ?box ?statement)))
(<= (accessibleBox ?box)
(true (currentBox ?box)))
(<= (accessibleBox ?outerBox)
(true (boxIsInside ?innerBox ?outerBox))
(accessibleBox ?innerBox))

Meanwhile, opening and closing boxes would be moves and would need transitions that managed the state of e.g. currentBox and boxIsInside. (Note that you can only give the player a finite number of possible assumptions to make when opening a box...)

I actually had this window open for just over an hour and I didn't see your reply.
The solution I'm going for at the moment has an 'assume A' to open a box and 'assumption A X' for what happens in the box.
That leads, assuming it works as intended, to something like 'assumption (((A) B) C) X' down the line.
That would be more like the list approach you say is unstable right?

Yes, sorry it's not very clear.
Here is an example for -> intro, I haven't tested it yet but it's representative of the idea I'm going for atm.
vps1.piater.name/commie/#kvTJybkb
It seems very similar to your idea of linked list unfortunately :/

I see.
Testing the game with the best players is a side goal so I might have to rewrite this.
Thanks.

I notice that in those rules, you are using both (true (formula _)) and (formula _) as sentence types. These do not mean the same thing, and should not be included in the same game, to avoid confusion. There are really two types of sentences; "true" was perhaps a poor choice of keyword, as it means something closer to "state". Sentences with the names "true", "init", and "next" deal with the state of the game, while sentences lacking that are part of the game logic within a given turn.

If you want something that expresses all the types of formulas that could exist, you normally want this to be a bit of logic that is separate from the game state. (That is, use "(formula _)" and not "(true (formula _))".) For example, tic-tac-toe uses an (index _) sentence to indicate 1, 2, and 3 as the possible x- or y-coordinates. Chess similarly has (rank _) and (file _) sentences for this. It would probably be helpful to have (proposition p), (proposition q), etc. as a starting point, listing the individual claims that might be assumed to be true or false.

For the rule at the end, (not (known ?x)) should be (not (true (known ?x))).

(Extra note: You don't need to include "control" state if it remains the same every turn. It has no meaning beyond how it is used elsewhere in a game description.)