Thanks for the reply and pointers.

The intro to TFA> To most AI researchers, the frame problem is the challenge of representing the effects of action in logic without having to represent explicitly a large number of intuitively obvious non-effects. But to many philosophers, the AI researchers' frame problem is suggestive of wider epistemological issues. Is it possible, in principle, to limit the scope of the reasoning required to derive the consequences of an action? And, more generally, how do we account for our apparent ability to make decisions on the basis only of what is relevant to an ongoing situation without having explicitly to consider all that is not relevant?

Near as I can tell separation logic (suitably generalised/tamed/adapted to suit the system of interest/tools in use) addresses all these concerns. I'm not claiming it solves every last variant of the frame problem that anyone has ever considered; just that it seems to address the classical concerns about modularly specifying the effects of actions.

Take, for instance, the last question: separation logic models this by explicitly splitting the state (of the system of interest) into "relevant" and "not relevant" via separating conjunction (etc) and the suggestively-named "Frame" axiom takes care to preserve the "not relevant" part.

This partially addresses epistemics too, but I see that an action may affect things that I am not aware of. Though perhaps that is more of a modelling issue than a linguistic one.

I have no clue what does and does not work well with LLMs -- I'm just talking about explicit symbolic representation and (computer assisted/mechanised) reasoning; GOFAI but from a program logic perspective. Are you claiming that separation logic is unusable by LLMs? Or that it isn't helpful for capturing some essential aspects of framing in real-world problems?