Prolog Tribute to Hao Wang

General
1

This code here doesn’t make much sense:

One can combine member/2 and del/3 into select/3. select/3
together with member/2 is part of the Prologue to Prolog:

A Prologue for Prolog (working draft)
https://www.complang.tuwien.ac.at/ulrich/iso-prolog/prologue

So if I further strip away using a two sided sequent,
I can implement Hoa Wangs implication fragment:

image

image

(Hao Wang. Toward Mechanical Mathematics. IBM
Journal of Research and Development 4:1 (1960), 15.)

as follows in 3 lines:

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), !.

Seems to work, I can prove Peirce Law:

?- prove([(((p->q)->p)->p)]).
true.

See also:

Hao Wang on the formalisation of mathematics
Lawrence C. Paulson 26 Jul 2023
https://lawrencecpaulson.github.io/2023/07/26/Wang.html