Advent of Logic 2024: Weekend 1

[Mild Shock]

Hi,

Draw a Colored ASCII Christams tree with Prolog.

Bye

[Mild Shock]

Hi,

Create a proof search in Combinatory Logic,
that finds a Combinator Expression as proof
for a given formula in propositional logic.

The propositional logic can do with
implication only, and it should be Linear Logic.
French logician Jean-Yves Girard is credited

with Linear Logic, and since we have implication
logic only, the Logic will be also affine, i.e.
it will have no contraction, which makes

it special towards certain paradoxes.

Bye

Post by Mild Shock
Hi,
Draw a Colored ASCII Christams tree with Prolog.
Bye

[Mild Shock]

Hi,

Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.

The logic is the same as in Weekend 2.

Bye

Post by Mild Shock
Hi,
Create a proof search in Combinatory Logic,
that finds a Combinator Expression as proof
for a given formula in propositional logic.
The propositional logic can do with
implication only, and it should be Linear Logic.
French logician Jean-Yves Girard is credited
with Linear Logic, and since we have implication
logic only, the Logic will be also affine, i.e.
it will have no contraction, which makes
it special towards certain paradoxes.
Bye

Post by Mild Shock
Hi,
Draw a Colored ASCII Christams tree with Prolog.
Bye

[Mild Shock]

Hi,

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

Bye

Post by Mild Shock
Hi,
Create a proof search in Simple Types,
that finds Lambda Expressions as proof,
for a given formula in propositional logic.
The logic is the same as in Weekend 2.
Bye

Post by Mild Shock
Hi,
Create a proof search in Combinatory Logic,
that finds a Combinator Expression as proof
for a given formula in propositional logic.
The propositional logic can do with
implication only, and it should be Linear Logic.
French logician Jean-Yves Girard is credited
with Linear Logic, and since we have implication
logic only, the Logic will be also affine, i.e.
it will have no contraction, which makes
it special towards certain paradoxes.
Bye

Post by Mild Shock
Hi,
Draw a Colored ASCII Christams tree with Prolog.
Bye

[Mild Shock]

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

Post by Mild Shock
Now that Christmas is over, are you excited for the new year?
- Do the same as for Weekend 2 and Weekend 3
for a relevant logic.
Logic Weakening Contraction
Minimal Yes Yes
Relevant No Yes
Affine Yes No
Linear No No

[Mild Shock]

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

Post by Mild Shock
Now that Christmas is over, are you excited for the new year?
- Do the same as for Weekend 2 and Weekend 3
for a relevant logic.
Logic Weakening Contraction
Minimal Yes Yes
Relevant No Yes
Affine Yes No
Linear No No