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

On 22/11/2024 18:23, Julio Di Egidio wrote:

On 19/11/2024 14:55, Mild Shock wrote:

Julio Di Egidio schrieb:

On 19/11/2024 12:25, Mild Shock wrote:

Can λ-prolog do it? The proof is a little bit
tricky, since line 1 is used twice in
line 2 and in line 4. So its not a proof
tree, rather a proof mesh (*).

>
My reduction rules actually take a goal and, if it can be reduced,
return proof steps and residual goals.  But indeed, my experiment
has started with "how far can I get without lambda Prolog", aka "why
lambda Prolog?"

>
I don't know exactly what your full source
code in plain Prolog is.

>
It's here for your preview, up to disjunction and with a beginning of
a proof tree (still with the messed up numbering):
>
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
>
And it fails one test:
>
```
?- solve_t.
pos:begin:
- absorpt   : [(p->q)]=>p->p/\q             : ok
- andcomm   : [p/\q]=>q/\p                  : ok
- codilem   : [(p->q),(r->s),p\/r]=>q\/s    : FAIL!
- distand   : []=>p/\(q\/r)<->p/\q\/p/\r    : ok
- distor    : []=>p\/q/\r<->(p\/q)/\(p\/r)  : ok
- export    : [(p/\q->r)]=>p->q->r          : ok
- import    : [(p->q->r)]=>p/\q->r          : ok
- frege     : [(p->q->r)]=>(p->q)->p->r     : ok
- hsyllo    : [(p->q),(q->r)]=>p->r         : ok
- idempand  : []=>p/\p<->p                  : ok
- idempor   : []=>p\/p<->p                  : ok
pos:end: tot.=11, failed=1 : FAIL!
neg:begin:
- pierce    : []=>((p->q)->p)->p            : ok
neg:end: tot.=1, failed=0 : ok
false.
```
>
And I have already spent a day trying to find the bug, the trace is a
little bit overwhelming:
>
```
?- solve_trace([p->q,r->s,p\/r]=>q\/s, Qs).
```

>
Never mind, I have fixed it: just needed to get rid of those `once`!
Will update the Gist shortly.
>
If you have any feedback already, it's very welcome: anyway, will keep
you guys posted.
>
-Julio
>