In some cases the formal structure of expressions is not the most effective way of communicating particular features of the consequences derived from formal models. Diagrams can sometimes be used to highlight the most pertinent features. In Section 2.4.1 we use tree diagrams to summarise the proof trees for particular inference strategies and to highlight inconsistent steps. Similar diagrams are used in Sections 3.4, 3.6 and 3.8 to describe more conventional proof strategies. In Section 3.9.2 we summarise the results of a basic inductive generalisation method by plotting the paths from conditions to conclusions using a tree-structured notation. Section 4.1.4 uses a box and arrow diagram to show permitted sequences of processes from a given initial state, with branches making it easy to spot non-determinism in the model. A simpler, linear, sequence is used to show individual causal chains when exploring causal interactions between requirements and design in Section 5.3. Section 5.2.1 contains a plot of the solutions obtained from a numerical model against time, while Section 7.1.2 uses a diagram to annotate the components of another numerical model with descriptions of some sources of uncertainty in their definition.