Proof Transformations from Search-Oriented into Interaction-Oriented Tableau Calculi

Gernot Stenz (Munich University of Technology, Germany)

Wolfgang Ahrendt (University of Karlsruhe, Germany)

Bernhard Beckert (University of Karlsruhe, Germany)

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

Keywords: automated deduction, proof presentation, proof search, proof transformation, tableau calculi

Categories: I.2.3