2026-07-21T19:24:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6580 2024-03-06T10:38:46Z ddc:004 open_access

Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic Baillot, Patrick Das, Anupam proof theory linear logic bounded arithmetic polynomial time computation implicit computational complexity We prove a general form of 'free-cut elimination' for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing theorem for a fragment of this arithmetic via the `witness function method', showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of 'safe' recursive functions, due to Bellantoni and Cook, where the ! modality of linear logic corresponds to normal inputs of a safe recursive program. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Patrick Baillot and Anupam Das 2016 Is Part Of LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2016.40 urn:nbn:de:0030-drops-65807 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.40 eng https://creativecommons.org/licenses/by/3.0/legalcode