### 4.1 Free variable systems

The free variable sequent calculus adopts the structural LK rules in figure 1 with the proviso that the rules now operate on labelled formulae. Contraction hence looks like this:

$\begin{array}{cc}\frac{\text{\Gamma},A\left[p\right],A\left[p\right]\top \text{\Delta}}{\text{\Gamma},A\left[p\right]\top \text{\Delta}}LC& \frac{\text{\Gamma}\top A\left[p\right],A\left[p\right],\text{\Delta}}{\text{\Gamma}\top A\left[p\right],\text{\Delta}}RC\end{array}$

The logical rules are given in figure 6. Recall that the symbol p ranges over labels, which means that it can be either ε or a prefix term or a sequence of prefix terms. The inferences of type R⊃ and R¬ are parameter–labelled. Instances of L⊃ and L-¬ are variable–labelled. If r is one of the parameter–labelled ...

Get *Handbook of Automated Reasoning* now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.