The language of inference rules are much more general than what is usually given in Logic. Indeed you can look at systems with rules of the shape
$$ \frac{\Theta_1\ldots \Theta_n}{\Theta}$$
Where the $\Theta_i, \Theta$ are some kind of statement and ask: what are all the possible $\Theta$ I can get by repeated application of these rules?
In the above case, $s \vdash M \Downarrow P, s'$ expresses the statement:
With starting state $s$, program $M$ evaluates to $P$ and the resulting state is $s'$.
This is a very general framework for expressing the operational semantics of a program, and it means that if you can build a finite derivation tree with $s \vdash M\Downarrow P, s'$ at the base, then you have shown that the program $M$ is well-defined and evaluates to $P$.
Let's give an example. Say $s$ is the state in which variable $b$ is sent to true and $n$ is sent to $2$, which I will write $\{b\mapsto \mathrm{true}, n\mapsto 2 \}$. Then the following should be derivable:
$$\{b\mapsto \mathrm{true}, n\mapsto 2 \}\vdash \mathrm{if}\ b\ \mathrm{then}\ n+1\ \mathrm{else}\ 0 \Downarrow 3, \{b\mapsto \mathrm{true}, n\mapsto 2 \}$$
Note that in your question, the rule:
$$\frac{s_0 \vdash M_1 \Downarrow P_1, s_1 \; ... \; s_{n-1} \vdash M_n \Downarrow P_n, s_n}{s_0 \vdash M \Downarrow P, s_n}$$
Means:
If, starting from state $s_0$, $M_1$ reduces to $P_1$ and new state $s_1$, and starting with state $s_1$ $M_2$ reduces to $P_2$ and new state $s_2$ etc. then starting from state $s_0$, $M$ reduces to $P$ with new state $s_n$.
In particular, the order in which you do the reduction is important: the state may change after the evaluation of $M_1$, which in turn will influence the evaluation of $M_2$, etc. This is why in a language with state (side-effects), the order of evaluation of arguments passed to a function is important: we may get a different result depending on which argument we evaluate first.
In Haskell, laziness makes it impossible to know which arguments will be evaluated first (or at all!), so having side effects is pretty much out of the question.
I suggest reading the classic Types and Programming Languages, by Benjamin Pierce, which treats all of this in much detail.
