Re: can λ-prolog do it? (Was: How to prove this theorem with intuitionistic natural deduction?)

On 27/11/2024 18:58, Ross Finlayson wrote:

On 11/27/2024 04:06 AM, Julio Di Egidio wrote:

>
Hi Ross, it's a little linear propositional solver at this stage, but
with ambitions...

 Of course a variety of what are "non-standard", results, according
to the standard, are standard again, establishing the very ideals
and "goals" of inference, intuitionistic in the sense of a
"fuller dialectic".

I think my system is actually affine, not linear.
Whichever, that up to computability logic is the key idea:
<https://en.wikipedia.org/wiki/Substructural_type_system>
Anyway, experimenting while learning...  Indeed,
"I just write code that works, theory comes later".
Thanks for the feedback.
-Julio