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

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)))
Julio Di Egidio schrieb:

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).
```
 -Julio