Improving Wang's algorithm in Prolog

joseph-vidal-rosset · September 5, 2020, 7:05am

Here is Ben Hudson’s code I made the mistake of changing

%rule for id*
prove(L => R):-
	member(X,L),
	member(X,R),
	nl,write('=\tDone (by id*)').

But reading more carefully what you wrote, Jan, I realize that this code is maybe not much better : is it not also based on unification? You reply will help me to see if I need again to understand better what unification means.

Naoyuki Tamura seqprover.pl :

% Logical axiom
% cannot be invertible owing to unification
rule([cl,prop], no, ax, S, [], [[]]) :-
	match(S,  ([_X1,[A],_X2]-->[_Y1,[A],_Y2])).

I quote an email that I received from Naoyuki in 2019 July:

Dear Joseph,
I think you found a serious bug of seqprover.
For example, “X@p --> p” can be proved, but “X@Y@p --> p” cannot.
On the other hand, “all(X, all(Y, p)) --> p” can be proved by
llprover.
So, there should be something wrong in the program of seqprover.
don’t have a time to look at the code now, I will fix it in future.
Thanks again for your report.
– Naoyuki

I confirm that this problem has not been solved, unfortunately:

?- prover.
Sequent Calculus Prover ver 1.0 for SICStus Prolog
        by Naoyuki Tamura (tamura@kobe-u.ac.jp)
cl(first)> X@Y@p --> p.
_2032@_2026@p-->p.
Trying to prove with threshold = 0 1 2 3 4 5
Fail to prove _2032@_2026@p --> p (22 msec.)
yes
cl(first)> |:

joseph-vidal-rosset · September 5, 2020, 7:18am

Ben Hudson’s Wang prover works only with atoms, but it would be maybe still more efficient with Prolog variables, à la Jan Burse, as you showed to us very clearly.

joseph-vidal-rosset · September 5, 2020, 8:01am

Two different topics.

What symbolism should be adopted for propositional formulas, I mean : upper case letters or lower case letters ? They are many textbooks in logic (including Quine’s) where the second option is adopted, upper case letters being used only for predicates of the first order predicate calculus. From the point of view of Proof Theory, that is a bad option: Propositional Calculus is a part of First-Order Logic and propositional formulas can also been seen as predicates with arity zero. This is the point of view of David Nour and Raffalli in their excellent book “Introduction à la Logique, Théorie de la démonstration”, this is a convincing point of view.
What should be adopted by Prolog provers to implement the propositional calculus: Prolog variables or atoms? Jan Burse’s work on Quine prover has convinced me that the option of Prolog variables is far better.

We are lucky; the answers of point 1 and point 2 are in harmony.

joseph-vidal-rosset · September 5, 2020, 8:10am

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.

joseph-vidal-rosset · September 5, 2020, 8:59am

I feel lost. Tamura’s sequent system disables contraction, if I am not mistaken. The problem is therefore certainly in his Prolog code.

EricGT · September 5, 2020, 10:05am

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?

EricGT · September 5, 2020, 10:15am

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.

joseph-vidal-rosset · September 5, 2020, 10:17am

I will do nothing. Except to say that the documentation topic must be closed now on this thread. I thank again everybody.

joseph-vidal-rosset · September 5, 2020, 6:51am

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.

joseph-vidal-rosset · September 5, 2020, 11:51am

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).
% -----------------------------------------------------------------

joseph-vidal-rosset · September 5, 2020, 11:54am

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.

joseph-vidal-rosset · September 5, 2020, 12:38pm

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?

EricGT · September 5, 2020, 12:49pm

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.

joseph-vidal-rosset · September 5, 2020, 12:51pm

The best would be to move any post mentioning Wang prover to this page:

EricGT · September 5, 2020, 12:59pm

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 Wang for the search phrase.

A list of topics should display.

Don’t forget to click More at the bottom.

joseph-vidal-rosset · September 5, 2020, 1:06pm

@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

EricGT · September 5, 2020, 1:11pm

The starting post is #161 and the ending post is #174

joseph-vidal-rosset · September 5, 2020, 1:11pm

That’s correct !

joseph-vidal-rosset · September 5, 2020, 2:40pm

Yes. This prover is not good as soon as the formula is not valid…

joseph-vidal-rosset · September 5, 2020, 6:02pm

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))) . 
?-