JUCS - Journal of Universal Computer Science 5(3): 113-134, doi: 10.3217/jucs-005-03-0113
Proof Transformations from Search-Oriented into Interaction-Oriented Tableau Calculi
expand article infoGernot Stenz‡, Wolfgang Ahrendt§, Bernhard Beckert|
‡ Munich University of Technology, Munich, Germany§ Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, Karlsruhe, Germany| University of Karlsruhe, Karlsruhe, Germany

Corresponding author: Gernot Stenz

© Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckert.
This article is freely available under the J.UCS Open Content License.
Citation: Stenz G, Ahrendt W, Beckert B (1999) Proof Transformations from Search-Oriented into Interaction-Oriented Tableau Calculi. JUCS - Journal of Universal Computer Science 5(3): 113-134. https://doi.org/10.3217/jucs-005-03-0113
Open Access
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, tableau calculi, proof transformation, proof presentation, proof search