Affine Logic, what Properties does it have? (Was: Counter Example by Troelstra & Schwichtenberg)

Ok, this here is classical logic,
deterministically expressed:
prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(-A,L,R), member(A,R), !.
It can readily prove Peirce Law:
?- prove([(((p->q)->p)->p)]).
true.
With Coq or Isabelle/HOL you should be
also able to prove these meta theorems about
the Prolog predicate prove/1:
     prove([...,X,Y,...])
    ----------------------- (Exchange)
     prove([...,Y,X,...])
     prove([...,X,X,...])
    ----------------------- (Contraction)
      prove([...,X,...])
      prove([...,X,...])
    ----------------------- (Weakening)
     prove([...,Y,X,...])
https://en.wikipedia.org/wiki/Structural_rule
If you replace prove/1 with a deterministic prover
for affine logic, I guess you will still be
able to verify (Exchange) and (Weakening) for
an arbitary input. But not anymore (Contraction)
in general. What is the deterministic prover for
affine logic?
Julio Di Egidio schrieb:

On 04/12/2024 08:47, Mild Shock wrote:
 

Now I tried an example by Troelstra & Schwichtenberg:
>
solve_case(pos, schwichtenberg, [((((p->q)->q)->p)->q),(q->p)]=>q).
solve_case(neg, schwichtenberg2, [((((p->q)->q)->p)->q),(q->p)]=>q).
>
At least the second case shouldn't give false, as is seen here:

 It fails if you do (the equivalent of) the intros before the TNT: I had a doubt about that, thanks for the test case.  This works as expected:
 ?- solve([]=>tnt((((((p->q)->q)->p)->q)/\(q->p))->q)).
 -Julio