Algorithmic structuring of cut-free proofs


Computer Science Logic. 6th Workshop, CSL '92.
San Miniato. Selected Papers
(Springer, Berlin, 1993) 29-42
(with Matthias Baaz)


We investigate the problem of algorithmic structuring of proofs in the sequent calculi LK and LKB (LK where blocks of quantifiers can be introduced in one step), where we distinguish between linear proofs and proofs in tree form.