Proof Transformations from Search-Oriented into Interaction-Oriented Tableau Calculi
Дата
Авторы
Stenz,Gernot
Ahrendt,Wolfgang
Beckert,Bernhard
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
automated deduction , tableau calculi , proof transformation , proof presentation , proof search