I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes:In intuitionistic linear logic, environments are sets of available resources. In my logic, environments are partially ordered sets: some resources have to be consumed before others.Multiplicative conjunction splits into two connectives: parallel conjunction and sequential conjunction.Linear implication can only consume a resource X, if there is no other resource Y that must be consumed before X.Logical connectives are usually defined in terms of introduction and elimination rules. In my logic, I need a new kind of rule: usage rules, which describe how a resource can be used in a computation without destroying it.I add a new unary operator, called borrowed pointer, which denotes a non-owning reference to an existing resource.Creating a borrowed pointer uses but does not consume the resource being pointed. In particular, one may always create a borrowed pointer to an existing resource X, even if there is some resource Y that must be consumed before X.No resource may be consumed until all borrowed pointers to it have been consumed. This is my main motivation for introducing the notion of sequential conjunction in the first place.I want to give a formal presentation of the rules of inference of this logic using natural deduction and sequent calculus. However, I am having trouble coming up with a good notation that succinctly conveys ideas like:The environment $\Gamma$ can be split into sub-environments $\Delta, \Sigma$, where there is no resource in $\Sigma$ that must be consumed before any resource in $\Delta$.Given the environment $\Gamma$ and a resource $A \in \Gamma$, the result of adding a resource ${\rm ref} A$ to $\Gamma$, in such a way that ${\rm ref} A$ must be consumed before $A$.The sequential conjunction of $A$ and $B$.etc.What guidelines should I follow in order to design a good notation for this logic?
How to develop an effective notation for a partially ordered logic?
lo.logic;notation;sequent calculus;natural deduction