Algorithmic Structuring of Cut-free Proofs

In Egon Börger, Hans Kleine Büning, Gerhard Jäger, Simone Martini & Michael M. Richter (eds.), Computer Science Logic. CSL’92, San Miniato, Italy. Selected Papers. Berlin: Springer. pp. 29–42 (1993)
  Copy   BIBTEX


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) is investigated, where a distinction is made 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 length k , and l ≤ k : Is there is a proof 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 (corresponds to the undecidability of second order unification), (2) undecidable for linear LKB-proofs (corresponds to the undecidability of semi-unification), and (3) decidable for tree-like LKB -proofs (corresponds to a decidable subprob- lem of semi-unification).

Author Profiles

Richard Zach
University of Calgary


Added to PP

332 (#44,231)

6 months
45 (#77,518)

Historical graph of downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.
How can I increase my downloads?