Quelle est cette notation de style «Mathématiques discrètes» de type fraction utilisée pour les règles formelles?

Question

Dans le journal "Un type de données JSON répliqué sans conflit", J'ai rencontré cette notation pour définir formellement les "règles":

Comment s'appelle cette notation? Comment le lire?

Par exemple:

• la DOC La règle n'a rien dans son "numérateur" - pourquoi pas?
• la EXEC et GET Les règles semblent avoir deux termes distincts au-dessus de la ligne, qu'est-ce que cela signifie?
• la VAR La règle se démarque également un peu, car alors que de nombreuses autres règles utilisent une sorte de flèche (ce que je supporterais pour signifier "implique") en haut, celui-ci semble dire que X est un élément de quelque chose.
• presque tout est parsemé d'une initiale Ap, que le texte décrit comme "l'état de réplique p est décrit par AP, une fonction partielle finie" - comment un lecteur avisé de cette notation tenait-il à "voir" cette partie de chaque règle?

Ce site a suggéré une question connexe qui a une notation très similaire, sur la question Quelle est la signification de ⟨b, s⟩ -> ⟨b ', s'⟩ comme la règle initiale de cette question sur la sémantique en petite étape? - Ceci est étiqueté comme Sémantique opérationnelle, et cela semble être une bonne avance. Est-ce en effet le cadre dans lequel je devrais interpréter ces chiffres? Pourriez-vous facilement résumer cela sous forme de «cours intensif» afin que, même si je ne peux pas vérifier l'exactitude de leurs preuves, je pourrais au moins comprendre un peu plus ce qu'ils disent dans cette section?