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:
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.