Path: ...!news.misty.com!weretis.net!feeder9.news.weretis.net!news.quux.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: Negative translation for propositional linear (or affine) logic?
Date: Thu, 28 Nov 2024 03:01:19 +0100
Organization: A noiseless patient Spider
Lines: 21
Message-ID: <vi8itf$1n1h$4@dont-email.me>
References: <vhgdq0$19evr$1@dont-email.me> <vhgemi$ca9e$1@solani.org>
 <vhgg23$19evr$2@dont-email.me> <vhhsit$d108$1@solani.org>
 <vhhuuf$1qic1$1@dont-email.me> <vhi5ch$d5rb$1@solani.org>
 <vhqemf$16mc2$1@dont-email.me> <vi8bgs$42ft$1@solani.org>
 <vi8et8$1n1h$2@dont-email.me> <vi8h9s$ghq4$1@solani.org>
 <vi8hij$gi0t$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 28 Nov 2024 03:01:19 +0100 (CET)
Injection-Info: dont-email.me; posting-host="52d3d32bb300a58b1c7fce645c7cbe65";
	logging-data="56369"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/Zg/U4oOEmP2/otVKSOv8RWIHFmiIGNac="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:FXzQABE+id0tUPijYV9Khhxfva0=
In-Reply-To: <vi8hij$gi0t$1@solani.org>
Content-Language: en-GB
Bytes: 1823

On 28/11/2024 02:38, Mild Shock wrote:
> 
> In affine logic you can possibly do something like iterative
> deepening, only its iterative contraction.
> 
> Define A^n o- B as:
> 
> A o- A o- .. A o- B
> \-- n times --/
> 
> The running the prover with this notation:
> 
> A -> B  := A^n o- B
> 
> repeatedly with increasing n .

Yeah, something like that, but I am pretty sure we can do better than 
just trial and error.

-Julio