Path: ...!2.eu.feeder.erje.net!3.eu.feeder.erje.net!feeder.erje.net!usenet.goja.nl.eu.org!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: comp.lang.prolog
Subject: Prolog Tribute to Hao Wang
Date: Fri, 6 Dec 2024 21:15:37 +0100
Message-ID: <vivm19$t816$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 6 Dec 2024 20:15:37 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="958502"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:hDW8jiTlXR1BW6ndJN90GXWMoOM=
X-Mozilla-News-Host: news://news.solani.org:119
X-User-ID: eJwNxskRACEIBMCUGDmEcGBc8w9hfXRVuwaC28LD/PrN+R4pi1m0gtetk1Ng4LV7Jg5MxwXaKykAyd5JEw3+Wd0VjA==
Bytes: 2282
Lines: 43

This code here doesn’t make much sense:

prove(L --> R):-
	member(A => B,L),
	del(A => B,L,NewL),!,

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 fagment:

P1. Initial rule: if λ, ζ are strings of atomic
formulae, then λ -> ζ is a theorem if some atomic
formula occurs an both sides of the arrow.

P5a. Rule —> =>	If ζ, φ -> λ, ψ, ρ, then ζ -> λ, φ => ψ, ρ
P5b. Rule => -> If λ, ψ, ρ -> π and λ, ρ -> π, φ then λ, φ => ψ, ρ -> π

(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