What is this fraction-like “discrete mathematics”–style notation used for formal rules?

Question

In the paper "A Conflict-Free Replicated JSON Datatype", I encountered this notation for formally defining "rules":

What is this notation called? How do I read it?

For example:

• the DOC rule doesn't have anything in its "numerator" — why not?
• the EXEC and GET rules appear to have two separate terms above the line, what does that mean?
• the VAR rule stands out a bit as well, since while many other rules use some sort of arrow (which I would take to mean "implies") up top this one only seems to be saying that x is an element of something.
• almost everything is peppered with an initial Ap, which the text describes as "the state of replica p is described by Ap, a finite partial function" — how would a savvy reader of this notation tend to "see" that part of every rule?

This site did suggest a related question that has some very similar-looking notation, over on the question What is the significance of ⟨B, s⟩ -> ⟨B', s'⟩ as the initial rule in this question about small-step semantics? — this is tagged as Operational semantics, and that does seem to be a strong lead. Is that indeed the framework under which I should be interpreting these figures? Could you easily summarize this in "crash course" form so that, even if I can't verify the correctness of their proofs, I could at least get a bit more understanding of what they are saying in this section?