Optimization models are widely used in energy system planning to identify cost-effective investment strategies. However, relying solely on a single optimal solution can be misleading, as it fails to account for model uncertainty, competing objectives, and stakeholder preferences. To address this, near-optimal alternatives, solutions that are close in cost to the optimum but structurally different, are increasingly used to support robust and flexible decision-making.

This thesis explores the generation and evaluation of near-optimal alternatives within energy systems, with a focus on improving the decision relevance of the generated alternatives. This thesis introduces a unified analytical framework, formalizing existing Modeling to Generate Alternatives (MGA) methods using weight vector formulations. This formulation enables a clearer comparison of different techniques that generate these alternatives. This analysis highlights the limitations of current evaluation metrics, particularly their inability to distinguish decision-relevant alternatives from decision-irrelevant ones.

To overcome this gap, the thesis proposes a novel evaluation metric based on dominance relations from multi-objective optimization. This metric identifies non-dominated alternatives, those not strictly worse than any other across all decision variables, as decision-relevant. The thesis introduces a new method that uses Directionally Weighted Variables to generate alternatives aligned with this dominance criterion.

The proposed approach is evaluated using a stylized energy investment model and benchmarked against existing MGA techniques. Results show that traditional methods tend to generate fewer non-dominated alternatives, while the new method generates more non-dominated alternatives within the near-optimal space. This work contributes a new perspective on alternative generation, bridging the gap between mathematical optimality and practical decision support.

This paper focuses on implementing and verifying the proofs presented in ``Finite Sets in Homotopy Type Theory" within the UniMath library. The UniMath library currently lacks support for higher inductive types, which are crucial for reasoning about finite sets in Homotopy Type Theory. This paper addresses that issue and introduces higher inductive types to UniMath. This is used to develop a computer-checked implementation of the proofs within "Finite Sets in Homotopy Type Theory." This implementation enables future research on finite sets in HoTT by providing accessible and reliable proofs.

This paper defines finite sets as Kuratowski-finite. This is in contrast with the most common notion of finiteness, e.g. Bishop-finite and enumerated types. I argue that Kuratowski-finiteness is the most general finite for which the usual operations of finite types and sub-objects can be operated upon.