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)
Download Edit this record How to cite View on PhilPapers
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).
(categorize this paper)
PhilPapers/Archive ID
Revision history
Archival date: 2017-10-10
View upload history
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Added to PP index

Total downloads
28 ( #31,648 of 36,564 )

Recent downloads (6 months)
4 ( #33,613 of 36,564 )

How can I increase my downloads?

Monthly downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.