Improving Wang's algorithm in Prolog

Hello, I published here a Prolog implementation of Wang’s algorithm that was originally written by Ben Hudson and published here. Ben Hudson’s prover requested two inputs: first the set of premises as list, i.e. [formulas_premises], second the set of consequences as list [formulas_consequences]. I provided a simplification with writing a version that needs only one input: formula as list, that is or that is not a theorem. I noticed that this prover is rather efficient to prove, but fail to disprove big formulas. It would be also better to avoid the constrain of writing the formula to test in a Prolog list, IMHO. Here is Ben Hudson’s prover. Any improvement for performances or for proof format will be welcome.

% COMP 360 Final Project:
% A Propositional Theorem Prover using Wang's Algorithm
% Ben Hudson

:-op(700,xfy, => ). 
:-op(650,xfy,-> ). 
:-op(600,xfy,v). 
:-op(500,xfy,^).
:-op(450,fy,~).

%TYPE 'run.' INTO THE CONSOLE TO START

run:-
	write('\nA Propositional Theorem Prover using Wang\'s Algorithm\n'),
	write('\tby Ben Hudson\n\n'),
	getPremises(T).

getPremises(Premises):-
	write('Input premises, as a list (e.g. [a ^ b, c]): '),
	nl,
	read(Premises),
	nl,
	getTheorem(Premises,X).

getTheorem(Premises,Theorem):-
	write('Input theorem to be proved, as a list: '),
	nl,
	read(Theorem),
	nl,
	write('To prove: '),
	nl,
	write(Premises => Theorem),
	go(Premises => Theorem).

go(X):-
	prove(X),
	write('\n\nWe can conclude that this is a theorem.\n').
go(X):-
	write('\n=\tCannot be proved.'),
	write('\n\nWe can conclude that this is not a theorem.\n\nInstance where this does not hold:'),
	reduce(X).

%predicate to delete an element X from a list L.
del(X,[X|Tail],Tail).
del(X,[H|Tl1],[H|Tl2]):-
        del(X,Tl1,Tl2).

%negation
prove(L => R):-
	member(~X,L),
	del(~X,L,NewL),
	nl,write('=\t'),write(NewL => [X|R]),
	write('\t (by negation/left)'),
	prove(NewL => [X|R]).
prove(L => R):-
	member(~X,R),
	del(~X,R,NewR),
	nl,write('=\t'),write([X|L] => NewR),
	write('\t (by negation/right)'),
	prove([X|L] => NewR).

%non-branching rules
prove(L => R):-
	member(A ^ B,L),
	del(A ^ B,L,NewL),
	nl,write('=\t'),write([A,B|NewL] => R),
	write('\t (by and/left)'),
	prove([A,B|NewL] => R).
prove(L => R):-
	member(A v B,R),
	del(A v B,R,NewR),
	nl,write('=\t'),write(L => [A,B|NewR]),
	write('\t (by or/right)'),
	prove(L => [A,B|NewR]).
prove(L => R):-
	member(A -> B,R),
	del(A -> B,R,NewR),
	nl,write('=\t'),write([A|L] => [B|NewR]),
	write('\t (by arrow/right)'),
	prove([A|L] => [B|NewR]).

%branching rules
prove(L => R):-
	member(A ^ B,R),
	del(A ^ B,R,NewR),
	nl,write('\tFirst branch: '),
	nl,write('=\t'),write(L => [A|NewR]),
	write('\t (by and/right)'),
	prove(L => [A|NewR]),
	nl,write('\tSecond branch: '),
	nl,write('=\t'),write(L => [B|NewR]),
	write('\t (by and/right)'),
	prove(L => [B|NewR]).
prove(L => R):-
	member(A v B,L),
	del(A v B,L,NewL),
	nl,write('\tFirst branch: '),
	nl,write('=\t'),write([A|NewL] => R),
	write('\t (by or/left)'),
	prove([A|NewL] => R),
	nl,write('\tSecond branch: '),
	nl,write('=\t'),write([B|NewL] => R),
	write('\t (by or/left)'),
	prove([B|NewL] => R).
prove(L => R):-
	member(A -> B,L),
	del(A -> B,L,NewL),
	nl,write('\tFirst branch: '),
	nl,write('=\t'),write([B|NewL] => R),
	write('\t (by arrow/left)'),
	prove([B|NewL] => R),
	nl,write('\tSecond branch: '),
	nl,write('=\t'),write(NewL => [A|R]),
	write('\t (by arrow/left)'),
	prove(NewL => [A|R]).

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

%reduces expression so you can print out what the false stuff is
reduce(L => R):-
	member(~X,L),
	del(~X,L,NewL),
	reduce(NewL => [X|R]). %negation left
reduce(L => R):-
	member(~X,R),
	del(~X,R,NewR),
	reduce([X|L] => NewR). %negation right
reduce(L => R):-
	member(A ^ B,L),
	del(A ^ B,L,NewL),
	reduce([A,B|NewL] => R). %and/left
reduce(L => R):-
	member(A v B,R),
	del(A v B,R,NewR),
	reduce(L => [A,B|NewR]). %or/right
reduce(L => R):-
	member(A -> B,R),
	del(A -> B,R,NewR),
	reduce([A|L] => [B|NewR]). %arrow/right
reduce(L => R):-
	member(A ^ B,R),
	del(A ^ B,R,NewR),
	reduce(L => [A|NewR]),
	reduce(L => [B|NewR]). %and/right
reduce(L => R):-
	member(A v B,L),
	del(A v B,L,NewL),
	reduce([A|NewL] => R),
	reduce([B|NewL] => R). %or/left
reduce(L => R):-
	member(A -> B,L),
	del(A -> B,L,NewL),
	reduce([B|NewL] => R),
	reduce(NewL => [A|R]). %arrow/left
reduce(L => R):-
	member(X,L),
	member(X,R).
reduce(L => R):-
	write('\nSet '),write(L),
	write(' as True, and '),write(R),write(' as False.').

Use format/2,3 instead of write/1.

Your way with write/1

help_01 :-
    write('-----------------------------------------------------------'),nl,
    write('\nA Propositional Theorem Prover using Wang\'s Algorithm\n'),
    write(' \tby Ben Hudson\n\n'),
    write('-----------------------------------------------------------'),nl,
    write('To test the validity of your formula with Wang\'s algorithm:\n'),
    write('- First, write "wang." and press Enter.\n'),
    write('- Second, with this usual syntax: ~ a | a &  b | a v b | a -> b \n'),
    write('put your formula into square brackets (e.g. [p -> p]), press Enter.\n'),
    write('That\'s it. Have fun!').

Using format/2,3

help('\c
    -----------------------------------------------------------\n\n\c
    A Propositional Theorem Prover using Wang\'s Algorithm\n\c
    \tby Ben Hudson\n\n\c
    -----------------------------------------------------------\n\c
    To test the validity of your formula with Wang\'s algorithm:\n\c
    - First, write "wang." and press Enter.\n\c
    - Second, with this usual syntax: ~ a | a &  b | a v b | a -> b \n\c
    put your formula into square brackets (e.g. [p -> p]), press Enter.\n\c
    That\'s it. Have fun!\c
').

help_02 :-
    help(Help),
    format('~a',[Help]).

\c is not common.
See: Character Escape Syntax

I am also thinking you should replace read/1 which reads Prolog terms with DCGs because many people don’t understand what a Prolog term is, they get frustrated quickly and walk away when seeing error messages that don’t help them understand how to change the input to make it valid.

If you are taking the time to make the code work then take the time to make the user interface user friendly. I can’t count how many times I have walked away from code that I know is of use just because it was not easy to use or understand.

Learning DCGs could take days to weeks to get correct depending on your skill level, but having been their and having done the work it is worth it. If you search the SWI-Prolog code at GitHub for --> (search) you will see how often they are used because DCGs are just that useful.

As an example of learning something different to get the user interfaces to be nice, for many years I have been using GraphViz to display graphs. Since Prolog is about relationships and Graphs are great for drawing relationships, the synergy is great. But one of the things that leaves a bad taste in my mouth with GraphViz is that the graphs are static, typically displayed as PNG, PDF, or SVG.

Graphs should allow a user to move the nodes around and so the last several days I have been learning how to convert Prolog facts into Cytoscape.js graphs. Quite the learning experience. But once done I will update the Wiki page and we will all have more knowledge to draw upon when using Prolog with Cytoscape.js. I must note that @CapelliC did something similar for SWISH (ref).

Also you might want to consider having your code work on SWISH. Don’t ask me about SWISH as I don’t use it currently. Not that I don’t want to, but one can only do so much at a time.

If you want to get more advanced with printing messages, see: Printing Messages in SWI-Prolog

2 Likes

Thanks for the links and for your suggestions to improve the interface of this program. I share your opinion about the importance of this point.
I did not understand how works format/2,3 and I must say frankly that the official documentation of SWI-Prolog lacks of clear and simple examples for people who try to learn Prolog: predicates are formally described, but some lines of code in some short programs would be helpful and often there is no the least example to get the use of such or such predicate. That is very frustrating.
I knew the existence of DCGs, but I believed that they was useful only in analysis of language.
I will read Printing Messages in SWI-Prolog . Pretty-printing in Prolog is not easy to understand and in spite of examples using of pretty-printing masterfully as for example Naoyuki Tamura’s sequent prover this art is far beyond my skills and I know no documentation to learn it.

1 Like

Just ask, we don’t bite.

Many of us understand what you are saying (ref) and it does take time to learn how to read the documentation.

Now for the hard part, if you start to learn how to use the predicates such as format/2,3 that you don’t know how to currently use, then you should add example comments on the documentation pages, add to post here in categories such as Nice to know, Useful Code, Wiki, create SWISH tutorial, create GitHub gist, create GitHub repositories, add to Useful Prolog References, etc.

Have you ever heard the quote about being a master of something.

A master has done it more ways wrong than a beginner has done it.

I can assure you I have done Cytoscape.js more ways wrong in the last several days than I have done it right, but I did just added a post in preparation for the Wiki.

While you may not see it, you are not alone in a crowed boat, the difference is you are at least asking questions and trying to learn, I can’t tell you how many times I hear from others that they started to learn Prolog and then gave up but wish they had the will-power to stay with it. :slightly_smiling_face:

Think about where you were when you asked the question at StackOverflow and where you are now.

1 Like

This is a valid observation. Keep in mind that the official documentation is documenting the SWI-Prolog implementation of the Prolog programming language, it isn’t meant to be a book on Prolog programming.

At the home page, there is a drop down menu “Tutorials”; hover with your mouse to look at it (because modern web). The most complete material there is under “External collections” -> “Meta level tutorials”. Here is a direct link: https://www.metalevel.at/prolog. This is a very good resource for learning, even if it is a bit terse. It covers DCGs in detail (tersely).

But wait, there’s more! There is a lot of code in the SWI-Prolog libraries. Just go ahead and read it!

You can find everything here:

One place to look is inside /library. Another place is the packages; they are in their own repositories. If you follow the instructions for building, “Preparing the source”, here: https://www.swi-prolog.org/build/unix.html you will get the complete source for SWI-Prolog and the packages on your own machine. This should be enough:

git clone https://github.com/SWI-Prolog/swipl-devel.git
cd swipl-devel
git submodule update --init

Once you have that, one thing you can do is do a full-text search for the predicate you want to know how to use. You will see how it is used in context.

I hope this helps.

1 Like

The Prolog community is wonderful. Many thanks to all of you.

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

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.

Two different topics.

  1. 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.

  2. 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.

Usually in a prover you have two types of variables

G  |- A(y), D
------------------  (∀R)       y ~e G,D
G |- ∀xA(x), D

G  |- A(t), D
------------------  (∃R)
G |- ∃xA(x), D

The variable from (∀R) has a side condition. You might connect with the folks of Qu-Prolog, they have added freeze and melt of variables.

Qu-Prolog Home Page
It is the implementation language for the Ergo theorem prover.
http://staff.itee.uq.edu.au/pjr/HomePages/QuPrologHome.html

A solution to the problem could be locking of a variable, so that it doens’t participate in unification, and then use unification in the (id) nevertheless.

Didn’t try yet locking, some people use also gensym and turn the variable into a new atom, this also prevents unification.

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. :frowning:

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.

  1. The low-level C code which is typically in the /src directory
  2. The core Prolog code which is typically in /boot
  3. The libraries of Prolog code which is typically in /library
  4. 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)
  5. 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?

I don’t think a packs discussion has something to do with Wang’s algorithm.
Maybe you can split the topic.

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. :slightly_smiling_face:

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

You could try Jens-Otten’s Prover and feed it the negation of the formula. If he can prove the negation of the formula, then there is something wrong.

I think the formula is some of the smallest formulas that embodies the concept of vacous truth, which is not anymore a propositional truth, but needs some quantifier rules. While I wrote the working paper if I remember well I took the formula it from May’s dissertation, since I needed an example.

My working paper was a personal wrap up of May’s dissertation, which was made in the context of the emerging field of substructural logic. What striked me was the fact that structural inference rules are somehow connected to quantifiers and I wanted to personally re-explore this relationship.

Substructural logics have significance in relevance logic and linear logic.

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.

The Wang code, besides of some of its drawbacks, is nice. Since it also provides a model finder. I tried it, and it almost works. But pitty you changed the arrow from --> to =>, which nearly got me:

?- reduce([]=>[p v ~q]).

Set [q] as True, and [p] as False.
true ;

Set [] as True, and [p,~q] as False. /* not intended output I guess */
true ;

Set [] as True, and [p v ~q] as False. /* not intended output I guess */
true.

But there are somewhere some cuts missing, since the further two lines seem not intended to me. Your reduce/1 is a nice alternative to my falsify/1.

Edit 05.09.2020:
Here you see the problem of unification. If we switch from Prolog atoms to Prolog variables, then the model finder isn’t working anymore like before:

?- reduce([]=>[P v ~Q]).
ERROR: Stack limit (1.0Gb) exceeded

It even crashes.

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