To simplify a bit, a system of inference rules generally defines a set of sequents, which are simply pairs of a list (or set) of propositions $\Gamma$ and a proposition $\phi$ written
$$ \Gamma \vdash \varphi$$
called the derivable sequents. The rules describe which sequents are derivable, and for any reasonable system, given $\Gamma\vdash\varphi$, and sequents $\Gamma_1\vdash\varphi_1,\ldots,\Gamma_n\vdash\varphi_n$, it is easy to tell whether
$$\frac{\Gamma_1\vdash\varphi_1\ldots \Gamma_n\vdash\varphi_n}{\Gamma\vdash\varphi} $$
is a valid derivation. This usually be done with some obvious algorithm.
Some much more difficult algorithmic questions are this:
- Given $\Gamma\vdash\varphi$, is this sequent derivable?
- Given $\Gamma$, how can we enumerate the set of $\varphi$ such that $\Gamma\vdash \varphi$ is derivable?
In general, there is no algorithm for answering question 1, and question 2 is quite difficult. In particular, when trying to prove $\Gamma\vdash\varphi$ a natural approach is to try to apply all possible rules until exhaustion. Several issues come up:
- What order do we apply rules in?
- How do we guess the $\Gamma_i\vdash \varphi_i$? If any variables appear on top that do not appear in the conclusion, you need to guess some instance for that variable.
- When do we know if a derivation does not exist?
Because of the complexity of these issues, it's much more natural to separate the system of rules that describe the derivable sequents from the algorithms trying to find actual derivations of a given sequent.