<p>It is notation for <a href="http://www.ams.org/notices/200811/tx081101370p.pdf" rel="nofollow">Formal Proofs</a> and specification of language grammar in <a href="http://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form" rel="nofollow">Backus-Naur Form</a>.</p>

CC BY-SA 3.0
2013-12-07T08:24:07.457Z
2013-12-07T08:24:07.457Z
Pratik Deoghare
<p>The individual statements of the form $A\Rightarrow B$ are <strong>sequents</strong> and the things that look like fractions are <strong>inference rules</strong>.</p>

CC BY-SA 3.0
2013-12-07T09:12:21.703Z
2013-12-07T09:12:21.703Z
David Richerby
<p>I was reading a <a href="http://www.oracle.com/technetwork/java/jvmls2013vitek-2013524.pdf" rel="nofollow noreferrer">paper</a> about implementing the statistical programming language R on the JVM, and encountered this notation I haven't seen before (I'm not formally CS-trained). What is the name of notational style? I've seen it before in other papers--usually as it related to functional programming and the REPL.
<img src="https://i.sstatic.net/rmTOm.png" alt="enter image description here"></p>

CC BY-SA 3.0
2013-12-07T07:11:46.043Z
See [here1](http://www.math.fsu.edu/~pkirby/mad2104/SlideShow/s3_1.pdf) and [Backus-Naur form](http://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form).
Pratik Deoghare
CC BY-SA 3.0
2013-12-07T07:56:17.720Z
I had seen BNF before (Odersky did it in the Functional Programming Coursera), but usually it was written out into words, so I figured this was something different. Please paste your comment into a full answer and I'll accept it.
Christopher Aden
CC BY-SA 3.0
2013-12-07T11:16:05.817Z
I believe that the fraction notation for rules of inference was introduced by [R. Smullyan, _Theory of Formal Systems,_ 1961]. See also http://en.wikipedia.org/wiki/Formal_system as a starting point.
Radu GRIGore
CC BY-SA 3.0
2013-12-07T13:52:00.727Z
actually, the fractional notation was used already in Gentzen's paper (1934) on natural deduction and sequent calculus, which I think (but am not 100% sure) is the original source.
Noam Zeilberger
CC BY-SA 3.0
2013-12-07T21:57:14.683Z
Yes, I was wrong, sorry. Smullyan also said so here, in comments: https://www.youtube.com/watch?v=P8VBeGl9Law I had rather badly misinterpreted a remark in another paper.
Radu GRIGore
<notation>
What is this notation style called?
Christopher Aden
# What is this notation style called?

(Asked by: username_0 on 2013-12-07)

I was reading a [paper](http://www.oracle.com/technetwork/java/jvmls2013vitek-2013524.pdf) about implementing the statistical programming language R on the JVM, and encountered this notation I haven't seen before (I'm not formally CS-trained). What is the name of notational style? I've seen it before in other papers--usually as it related to functional programming and the REPL.
![enter image description here](https://i.sstatic.net/rmTOm.png)

**Tags:** notation

> **Comments:**
> **username_1**: See [here1](http://www.math.fsu.edu/~pkirby/mad2104/SlideShow/s3_1.pdf) and [Backus-Naur form](http://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form).  
> **username_0**: I had seen BNF before (Odersky did it in the Functional Programming Coursera), but usually it was written out into words, so I figured this was something different. Please paste your comment into a full answer and I'll accept it.  
> **username_2**: I believe that the fraction notation for rules of inference was introduced by [R. Smullyan, _Theory of Formal Systems,_ 1961]. See also http://en.wikipedia.org/wiki/Formal_system as a starting point.  
> **username_3**: actually, the fractional notation was used already in Gentzen's paper (1934) on natural deduction and sequent calculus, which I think (but am not 100% sure) is the original source.  
> **username_2**: Yes, I was wrong, sorry. Smullyan also said so here, in comments: https://www.youtube.com/watch?v=P8VBeGl9Law I had rather badly misinterpreted a remark in another paper.  

---

## 2 answers

### Answer by username_1 on 2013-12-07. Score: 4 | Accepted answer

It is notation for [Formal Proofs](http://www.ams.org/notices/200811/tx081101370p.pdf) and specification of language grammar in [Backus-Naur Form](http://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form).


---

### Answer by username_4 on 2013-12-07. Score: 0

The individual statements of the form $A\Rightarrow B$ are **sequents** and the things that look like fractions are **inference rules**.


---

