INVESTIGATIONS INTO THE COMPLEXITY OF SOME PROPOSITIONAL CALCULI

Abstract

Cut-free Gentzen systems and their semantic-oriented variant, the tableau method, constitute an established paradigm in proof-theory and are of considerable interest for automated deduction and its applications. In this latter context, their main advantage over resolution-based methods is that they do not require reduction in clausal form; on the other hand, resolution is generally recognized to be considerably more efficient within the domain of formulae in clausal form.