ABSTRACT
All the calculi we have looked at in the previous chapters were built on data structures such as (finite) sequences, (finite) multisets or (finite) sets. Now, we look at calculi that add grouping to sequences, that is, they have certain trees as their basic data structure. We call these systems consecution calculi, when we want to emphasize this specific feature. First, it may appear that grouping is a complication that creates various obstacles, for instance, for a straightforward proof of the cut theorem. But soon it becomes clear that keeping the data structure free from any implicit assumptions brings within reach logics that could not be formalized earlier. Consecution calculi are not only exciting and rewarding to work with, but they provide a more refined perspective on sequent calculi than the calculi we have dealt with in the preceding chapters.
