Algorithmic structuring of cut-free proofs

Source

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

Abstract

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.