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
Abstract
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).
Categories
(categorize this paper)
PhilPapers/Archive ID
BAAASO
Upload history
Archival date: 2017-10-10
View other versions
Added to PP index
2017-10-10

Total views
145 ( #30,283 of 54,658 )

Recent downloads (6 months)
23 ( #29,924 of 54,658 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.