Journal of Universal Computer Science
Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckert
Logic calculi, and Gentzen-type calculi in particular, can be
categorised into two types: search-oriented and interaction-oriented
calculi. Both these types have certain inherent characteristics stemming
from the purpose for which they are designed.
In this paper, we give a general characterisation of the two types and
present two calculi that are typical representatives of their respective
class. We introduce a method for transforming proofs in the
search-oriented calculus into proofs in the interaction-oriented
calculus, and we demonstrate that the difficulties arising with devising
such a transformation do not pertain to the specific calculi we have
chosen as examples but are general. We also give examples for the
application of our transformation procedure.