What is this fraction-like "discrete mathematics"–style notation used for formal rules? 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⟩ -&gt; ⟨B&#39;, s&#39;⟩ 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?
This is a standard notation for an inference rule.  The premises are put above a horizontal line, and the conclusion is put below the line.  Thus, it ends up looking like a "fraction", but with one or more logical propositions above the line and a single proposition below the line.  If you see a label (e.g., "LET" or "VAR" in your example) next to it, that's just a human-readable name to identify the particular rule.

You might also see this referred to as natural deduction or Gentzen-style natural deduction.

This is a common notation in the programming languages literature.  You'll see it all over the place.  It's very convenient for the kinds of conclusions and recursive-structured proofs that arise in that field.

You'll see this notation used to express axioms/rules. You can think of each axiom as a template with "meta-variables" (e.g., expr); you can replace each meta-variable with some syntax from the programming language (e.g., any expression that is valid in the programming language), and you'll get an instance of the rule.  The inference rule promises that if all of the propositions are above the line are true (for some instance of the template, where you consistently replace each metavariable with the same value throughout the rule), then the proposition below the line will be true, too.