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

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?"
Now, thanks also to your help, I have fixed my rule for `->E` and now my little solver in plain Prolog does it:
```plain
?- solve_test.
solve_test::pos:
- absorp: [(p->q)]=>p->p/\q --> true
- andcom: [p/\q]=>q/\p --> true
- export: [(p/\q->r)]=>p->q->r --> true
- import: [(p->q->r)]=>p/\q->r --> true
- frege_: [(p->q->r)]=>(p->q)->p->r --> true
- hsyll_: [(p->q),(q->r)]=>p->r --> true
solve_test::pos: tot.=6, FAIL=0 --> true.
solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.
true.
```
```plain
?- solve(([]=>(p->q->r)->p/\q->r), Qs).
Qs = [
     impi((p->q->r)),
     impi(p/\q),
     impe(1:(q->r)),
     impe(1:p),
     impe(2:r),
     impe(2:q),
     equi(2:r),
     ande(1:(p,q)),
     equi(2:q),
     ande(1:(p,q)),
     equi(1:p)
].
```
In fact, it's still in its infancy and the output is still a flat mess with wrong hypothesis numbering, but I will keep working on it with the idea of going well past just propositional: will start sharing as soon as I manage to implement negation, and a proper proof tree...
-Julio