University of Calgary
UofC Navigation

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.

In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k/l-compressibility: "Given a proof of ? ? ? of length k, and l < k: Is there is a proof of ? ? ? of length < l?" When restricted to proofs with universal or existential cuts, this problem is shown to be

  1. undecidable for linear or tree-like LK-proofs,
  2. undecidable for linear LKB-proofs, and
  3. decidable for tree-like LKB-proofs.

(1) corresponds to the undecidability of second order unification, (2) to the undecidability of semi-unification, and (3) to the decidability of a subclass of semi-unification.

Download from SpringerLink


Download Preprint

Download PostScript