Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: comp.lang.prolog
Subject: Combinatorial Simple Typed Solution (Was: Advent of Logic 2024:
 Weekend 1)
Date: Fri, 17 Jan 2025 11:59:35 +0100
Message-ID: <vmdd6m$35kl$1@solani.org>
References: <vjksgj$sgo6$3@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 17 Jan 2025 10:59:34 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="104085"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101
 Firefox/128.0 SeaMonkey/2.53.20
Cancel-Lock: sha1:ogoL8ZwGfxybIToBu8LBwCYyu3M=
In-Reply-To: <vjksgj$sgo6$3@solani.org>
X-User-ID: eJwNxIENACEIBLCVgON4GQdU9h/hTZMSobE/D4ZzOOqVaYG2ue96ujfTIFumD1AnsYKzChRXXeSIJO32Uf0BW/QVRw==
Bytes: 2347
Lines: 41


Programming languages such as Vault, Rust, etc.. have
recently popularized substructural logics. Their type
systems share various forms of resource awareness.

Propositional substructural logics were already
discussed when Jan Łukasiewicz and Carew Arthur Meredith
met in 1947 in Dublin. We will investigate such logics
with the help of Prolog.

Links to Dogelog Notebooks that capture the proof finder
and the model finder are given at the end of the post.
We have practically automatized the work of a Logician
in the middle of the previous century.

We could determine proper inclusions relationships
among the examined Minimal, Affine, Relevant and
Linear logics.

See also:

Substructural Logics via Dogelog Player
https://x.com/dogelogch/status/1880084983316115798

Substructural Logics via Dogelog Player
https://www.facebook.com/groups/dogelog

Mild Shock schrieb:
> Now that Christmas is over, are you excited for the new year?
> 
> Here is the task for Weekend 4:
> 
> - Do the same as for Weekend 2 and Weekend 3
>   for a relevant logic.
> 
> This would complete the picture, since we would have:
> 
> Logic           Weakening      Contraction
> Minimal         Yes            Yes
> Relevant        No             Yes
> Affine          Yes            No
> Linear          No             No