O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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:

Γ , A [ p ] , A [ p ] Δ Γ , A [ p ] Δ L C Γ A [ p ] , A [ p ] , Δ Γ A [ p ] , Δ R C

si94_e

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

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required