I am busy with other stuff (Was: can λ-prolog do it?)

I am busy with other stuff. I have
decided to postpone logic for a while.
So although it was very temping to download
you software, and then replace these line:
notation(dnt(X), ~X->(~(~X)))
solve_t__sel(neg, C=>X) :-
    solve(C=>dnt(X)).
https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11
By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
    solve(C=>gliv(X)).
I am afraid I have no time for that. You
could do it by yourself. Or what
until somebody else does it. What will be
the results?
Julio Di Egidio schrieb:

On 28/11/2024 00:55, Mild Shock wrote:

This is Peirce law:
>
((p->q)->p)->p
Peirce law is not provable in minimal logic.
>
But I guess this is not Glivenko:
notation(dnt(X), ~X->(~(~X)))
>
https://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic >
>
Glivenko would be simply:
notation(gliv(X), (~(~X)))
>

 We have gone over that already.  Either you have memory problems or you are purposely flooding the channel at this point.
 -Julio