If you find some time, it would be great that you have a look on Naoyuki’s program that is a rather big file for a Prolog prover, with a very very nice pretty printer. Naoyuki Tamura is a computer scientist and, by contrast with me, he is not a poor amateur. I am going to correct the errors I made on Ben Hudson’s program. I am ashamed. 
I feel lost. Tamura’s sequent system disables contraction, if I am not mistaken. The problem is therefore certainly in his Prolog code.
While the statement is correct, it hides a problem that can cause a new user some confusion and needs a bit of clarification. The problem is not with the quoted statement but the wording used in the SWI-Prolog documentation.
Currently the way I think of SWI-Prolog code posted at the GitHub repository is of several parts.
- The low-level C code which is typically in the /src directory
- The core Prolog code which is typically in /boot
- The libraries of Prolog code which is typically in /library
- The packages such as ODBC which are listed in /packages but the code is in separate repositories under the main SWI-Prolog repository, e.g. packages-odbc. These are selected during the build. When installing SWI-Prolog on Windows with the Wizard they are also referred to as components. (ref)
- Packs - which are add-ons and not in the SWI-Prolog repository. These are installed once SWI-Prolog is running.
The key thing to point out is that sometimes Packs are noted as Packages and that can be confusing. e.g.
If you do a Google search for SWI-Prolog packages you will most likely find the packs instead of the packages.
I only understood it when I was corrected for something I wrote in a post and then I took the time to understand it. See: Library, packages and packs?
As @joseph-vidal-rosset has expressed some concern with the SWI-Prolog documentation and this is his topic, the post is to help him understand. While I do agree that your point is valid, and I do have the ability as an admin to split the topic off, I will let @joseph-vidal-rosset decide. If he decides that this should be split, it shall be done. 
I will do nothing. Except to say that the documentation topic must be closed now on this thread. I thank again everybody.
The error is mine, not Ben Hudson’s. I was inspired by Jen Otten’s code:
% axiom
prove(G > D,_) :- member(A,G), member(B,D),
unify_with_occurs_check(A,B).
but again, I misunderstood maybe also Otten’s code and translated wrongly, because Jen Otten wrote another prover. I see that you explained your point on the page dedicated to the implementation of Wang prover. Thanks a lot for your patience.
Sorry. I apologize also to Jen Otten, because I did no say that the version of leanseq that I quoted is 3, it belongs to a conference on lean Otten’s provers and was not complete intentionally. See this intersting webpage.
The last version i.e 5 should complete in FOL and that is this one:
% -----------------------------------------------------------------
% leanseq.pl - A sequent calculus prover implemented in Prolog
% -----------------------------------------------------------------
% operator definitions (TPTP syntax)
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % implication
:- op( 500, fy, !). % universal quantifier: ![X]:
:- op( 500, fy, ?). % existential quantifier: ?[X]:
:- op( 500,xfy, :).
% -----------------------------------------------------------------
prove(F) :- prove(F,1).
prove(F,I) :- print(iteration:I), nl,
prove([] > [F],[],I,1,_).
prove(F,I) :- I1 is I+1, prove(F,I1).
% -----------------------------------------------------------------
% axiom
prove(G > D,_,_,J,J) :- member(A,G),
A\=(_&_), A\=(_|_), A\=(_=>_),
A\=(~_), A\=(!_), A\=(?_),
member(B,D),
unify_with_occurs_check(A,B).
% conjunction
prove(G > D,FV,I,J,K) :- select1(A&B,G,G1), !,
prove([A,B|G1] > D,FV,I,J,K).
prove(G > D,FV,I,J,K) :- select1(A&B,D,D1), !,
prove(G > [A|D1],FV,I,J,J1),
prove(G > [B|D1],FV,I,J1,K).
% disjunction
prove(G > D,FV,I,J,K) :- select1(A|B,G,G1), !,
prove([A|G1] > D,FV,I,J,J1),
prove([B|G1] > D,FV,I,J1,K).
prove(G > D,FV,I,J,K) :- select1(A|B,D,D1), !,
prove(G > [A,B|D1],FV,I,J,K).
% implication
prove(G > D,FV,I,J,K) :- select1(A=>B,G,G1), !,
prove(G1 > [A|D],FV,I,J,J1),
prove([B|G1] > D,FV,I,J1,K).
prove(G > D,FV,I,J,K) :- select1(A=>B,D,D1), !,
prove([A|G] > [B|D1],FV,I,J,K).
% negation
prove(G > D,FV,I,J,K) :- select1(~A,G,G1), !,
prove(G1 > [A|D],FV,I,J,K).
prove(G > D,FV,I,J,K) :- select1(~A,D,D1), !,
prove([A|G] > D1,FV,I,J,K).
% universal quantifier
prove(G > D,FV,I,J,K) :- member((![X]:A),G),
\+ length(FV,I),
copy_term((X:A,FV),(Y:A1,FV)),
prove([A1|G] > D,[Y|FV],I,J,K).
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
% existential quantifier
prove(G > D,FV,I,J,K) :- select1((?[X]:A),G,G1), !,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove([A1|G1] > D,FV,I,J1,K).
prove(G > D,FV,I,J,K) :- member((?[X]:A),D),
\+ length(FV,I),
copy_term((X:A,FV),(Y:A1,FV)),
prove(G > [A1|D],[Y|FV],I,J,K).
% -----------------------------------------------------------------
select1(X,L,L1) :- append(L2,[X|L3],L), append(L2,L3,L1).
% -----------------------------------------------------------------In the code that I adopted, --> is implication i.e. syntactic derivation symbol in sequent calculus, and => is conditional. But I must add also that all the merits of Wang’s prover are Ben Hudson’s, and I am afraid that almost all its defects are in the modification of code that I dared to write.
Thanks. I gave up the multiformula on the right in my Wang prover file. Is it possible for me to move all that on this page deals with Wang prover to the page dedicated to this topic?
You can do it by creating new post, cutting the text out of the old post, pasting the text into the new post then deleting the old post as you do not have moderator or admin rights and I will not temporarily grant them.
I can do it more efficiently as an admin but need more info.
Can you be more specific?
Which post do you need moved to which topic?
Note: In moving post I am given no choice on where they are placed in the topic, IIRC they stay as individual post and are added after the last post in the topic.
When you identify the post to move, identify them using the reference for the post. It is easier to identify the correct post that way as the reference is unique.
The best would be to move any post mentioning Wang prover to this page:
Sorry 
but you will have to identify each post individually. If I move post by others based on your statement then I have to deal with the problem. If you identify each post individually and then there is a problem with the owner of that post then I can let you resolve the problem with them. I don’t mind helping but I won’t do something that can causes me more work.
You can search for such post.
You have to be on the web site to do this.
- Click on the magnifying glass in the upper right.
- Select
Search this topic - Enter
Wangfor the search phrase.
A list of topics should display.
Don’t forget to click More at the bottom.
@EricGT from this post to the last post of this web page, all this stuff would be better placed on the page Improving Wang's algorithm in Prolog
That’s correct !
1 Like
Yes. This prover is not good as soon as the formula is not valid…
Impressive ! I am going to test it. Thanks Jan, thanks again !
Something goes wrong for me with leanseq2.pl:
?- prove(?[X]:![Y]:(p(X) | ~p(Y))).
ERROR: Syntax error: Operator expected
ERROR: prove(
ERROR: ** here **
ERROR: ?[X]:![Y]:(p(X) | ~p(Y))) .
?-
I forgot to say thank your Eric. I apologize !
Done, but here is the very surprising result:
?- true.
?- prove(p => p).
iteration:1
1: iteration:2
1: iteration:3
1: iteration:4
1: iteration:5
1: iteration:6
1: iteration:7
1: iteration:8
1: iteration:9
1: iteration:10
1: iteration:11
1: iteration:12
1: iteration:13
1: iteration:14
1: iteration:15
without stop...
Funny word.