 While the MALL logic is an expressive and novel logic, it is also decidable and, thus, not capable of capturing the unbounded behaviors  found in, say, mathematics and computer science. As described above,  the addition of the exponentials ! and ? enriches MALL to full linear  logic and to a setting where unbounded behaviors can be captured.  A second approach to extending MALL to capture unbounded behaviors  involves the addition of the least and greatest fixed point operators as logical connectives  directly into MALL. In order to properly characterize fixed points  as being either the least or the greatest, it is necessary for the inference rules for fixed points to be “higher-order” in  the sense that they involve invariants. Such an extension to MALL  (also with first-order quantification and term equality) has been developed by Baelde  (Baelde &amp; Miller,  2007;  Baelde 2012) and has been used to  provide a proof-theoretic foundation for model checking  (Heath &amp; Miller 2018). 