Why do people not use "partially directed" graphs? Are there structures in use which are a mix of directed and undirected graphs? I.e. the effective edge-set consists of both directed and undirected vertex pairs.
In the case that the graph is simple, you can maybe use two directed graphs to represent an undirected connection. But in general, if the number of edges counts, that doesn't work. 
I'm reading 'Graph Theory - Bondy & Murty' and have two editions two decades apart in front of me. Comparing them, I've noticed that they switched from the definition "Graph := triple $(V,E,\psi)$ with vertices $v,w\in V$, edges $e\in E$ and edge-assignment $\psi(e)=\{u,v\}$ " to "Graph := pair $(V,E)$  with vertices and edges, and with assignment in the context/meta-language". Wikipedia suggest using the triple definition and also names a third definition with a multiset - which is then conceptually different, as the edge set $E$ are merely pairs of vertices themselves, $e=\{u,v\}$. Did they make this change because there is an established notation now? What do papers in the field use as definition? How to theorem provers implement graphs, typically?
 A: This does exist; it's called a mixed graph.
However, I suspect the reason that these graphs are not very common is that in many scenarios, an undirected edge will be equivalent to two directed edges, one going in each direction.
A: I can provide you with a common use case of such mixed structures. 
When graphs are used as models of probability distributions, for example in Bayesian Networks, this happens quite often. In BNs we factorize a joint distribution (over the graph's nodes $x_i$) $$p(x_1,\ldots,x_n)$$ in terms of conditional distributions that encode the dependence in the edges of a directed acyclic graph: if $i \to j$, than $j$ conditionally depends on $i$. See the chain rule of probability.
So where do we find partially directed graphs? 
Well, we find them when we discover that 
some graphs induce the same $p(\cdot)$, regardless of the direction of some of their edges. This relates to the notion of v-structure $$X \to Y \quad \text{and}\quad Z \to Y$$ and I-equivalences, the corresponding equivalence classes with respect to $p(\cdot)$. 
Practically, such graphs are indistinguishable, in general, when we want to infer them from the data as we can not select within a class. When this happens, people often decide to switch representing such edges as undirected, rather than undirected, making the graph to be partially oriented, partially not. 
