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

Well my question was not really an advertisement
of λ-prolog, more an attempt to get assesment
of λ-prolog as viability for proof search.
I don't know exactly what your full source
code in plain Prolog is.
It seems to me λ-prolog has the following
pros and cons:
- Good: If the prover uses member/2 to access
   assumptions, or the list constructor to
   push assumptions, you can do this with
   embedded implication.
- Bad: If the prover uses select/3 things
   get nasty. Maybe a linar logic version of
   λ-prolog would help?
Bye
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?"
 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