a variable that is both universally and existentially quantified

[pfps]

There does not appear to be any requirement that the universal and existential variables of a graph are disjoint.

This makes the definition of isomorphism suspect as ({x},{x},{(x,:knows,:plato)}) apears to have the same meaning as ({},{x},{(x,:knows,:plato)}). Similarly the definition of normalization is also suspect. (Or maybe it is just normalization that should be changed.)

[doerthe]

Even with this interesting observation, the definitions as they are are still correct:
({x},{x},{(x,:knows,:plato)}) is isomorphic to ({y},{y},{(y,:knows,:plato)})
but not to
({},{x},{(x,:knows,:plato)})
The normalization of ({x},{x},{(x,:knows,:plato)}) is ({x},{x},{(x,:knows,:plato)}) .
From that perspective nothing is broken.

What is indeed counter intuitive and could (or even should?) be changed is that the normalization is defined in a way that it should remove all quantification variables which are not used when determining the semantics and the example shown contains the unused quantification set U={x}, that could be improved.