Implementing Quine's algorithm

I’m using: SWI-Prolog version : SWI-Prolog version 8.3.3 for x86_64-linux

I posted this question here, few days ago, but I’m wasting my time in trying to get a solution :

I am convinced that this task is not difficult for a good Prolog programmer, but I am not good at all and I would be happy to find help.

My main difficulty is to implement in Prolog the recursivity of Quine’s algorithm whose rules are applied to the connective of the smallest subformulas to the main connective of the formula (“from inside to outside”) , e.g.

                               (((a => b) => a) => a)
(((top => b) => top) => top)                (((bot => b) => bot) => bot)
  ((b => top) => top)                              ((top => bot) => bot)
     (top => top)                                       (bot => bot)
          top                                                     top

I would be glad to find a Prolog program for this algorithm (that traces tables for proof and disproofs), and in the same way, I would probably improve my understanding of Prolog.

In advance, thanks.
Jo.

2 Likes

At StackOverflow I am Guy Coder on this and many other forums I am EricGT. I moved away from using StackOverflow to improve my Prolog a few years ago as I found that I was picking up many bad habits and not really learning how to write real world Prolog. After being more active here my Prolog is moving in the right direction. Not afraid to take on some hard real world task, but do realize how much more I need to learn.


At SO you noted

I am afraid to fail to publish this prover in Prolog. My main difficulty is that I am unable to define recursively in the subformulas the reduction rules for propositional formulas. I am not competent enough to succeed, not because Quine algorithm is difficult to implement in Prolog, but because I am not competent enough in Prolog. It is very time consuming for me and all my tries are unsuccessful. :frowning:

While I can’t spend the time to work on this, I don’t mind giving some pointers.

The first thing I would do is try and break the algorithm down into parts that you do understand, then create test cases for them and write the code to pass the test case.

With regards to

My main difficulty is that I am unable to define recursively in the subformulas the reduction rules for propositional formulas.

I am thinking that the same logic used to reduce derivatives in Calculus could be used. (Just a guess.) However there is free code in this book on page 80.

“The Art of Prolog” By Leon S. Sterlingand and Ehud Y. Shapiro (site ) (free pdf )

Also take a look at the code for PRESS: PRolog Equation Solving System (Again just a pure guess)


I have to ask, How did you learn Prolog? mainly because Prolog is not like other programming languages and if you don’t learn the basics of syntactic unification, backtracking and cuts correctly you can spend years not really understanding Prolog.


I do have more than a beginner experience with logic simplification (ref 1) (ref 2) but it started with learning Digital Circuits with HeathKit and the last signfigant thing I did was translating the code in the “Handbook of Pratical Logic and Autmated Reasoing” from OCaml to F# with the help of a few others. I did check the book for Quine’s algorithm in case I forgot about it but it was not used so my memory is not failing.

I did see your reason why I should up the bounty ante by 200 points, but still am not convinced I should but still want to hear more.

In searching more for Quine’s Algorithm, it was not listed in Dictionary of Algorithms and Data Structures


If you have any questions just ask. I can’t guarantee that they will get a response but many do get a response.

Lastly, this is a forum for open discussion, so don’t feel you have to hold back for some obscure rules. Also if you post code you can always edit it after posting or delete it.


EDIT

After looking a bit more into Quine’s Algorithm, found the slide just before the one you noted.

http://cmsc-16100.cs.uchicago.edu/2017/Lectures/25/propositional-logic-quine-prover.php

If Quine’s Algorithm is really only just three rules of substitution, then then I think the links I referenced should get you past your block. Also if this is Quine’s only real use, then it is of vary limited use and I see no need to up the bounty by 200 points.


EDIT

The answer by Isabelle Newbie looks to have all of the valid parts. I did not check it for correctness.

If this were my question I would be looking for published problems of the type the algorithm can solve and set them up as test cases. I believe the first several in Seventy-Five Problems for Testing Automatic Theorem Provers would be of interest. Also check in The TPTP Problem Library
for Automated Theorem Proving


EDIT

Boolean Unification- The Story So Far (pdf) (Referenced by j4n_bur53 answer on StackOverflow).

2 Likes

First, many thanks for these very helpful references that will help me to improve my skills in Prolog, because I am not competent at the moment.
About Quine’s algorithm in “Methods of Logic”, I must stress on the point that its main interest is pedagogical. It is as easy to understand it as to apply it, by contrast with Quine – McCluskey algorithm. That’s it. I do not see what I have to add to explain Quine’s algorithm (tout court), it is very clear by itself.
I am happy to have raised your interest and to have learned from your replies.

Quine’s algorithm is contained in ten rules (without classical rules for negation). Why “only three rules of substitution”? I have described this algorithm in my first post.

Thanks for this clarification !

Here is the Prolog program given by Mostowski Collapse https://stackoverflow.com/users/502187/mostowski-collapseMostowski Collapse at the Stackoverflow webpage that I mentioned at the beginning of this post. I only changed the disjunction operator ! for ’ | ’ :

% operator definitions (TPTP syntax)

:- op( 500, fy, ~).     % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
% :- op(1110, xfy, =>).   % implication
% :- op(1110, xfy, <=>).  % biconditional

eval(A, A) :- var(A), !.
eval(A&B, R) :- !, eval(A, X), eval(B, Y), simp(X&Y, R).
eval(A '|' B, R) :- !, eval(A, X), eval(B, Y), simp(X '|' Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).

simp(A, A) :- var(A), !.
simp(A&_, 0) :- A == 0, !.
simp(_&B, 0) :- B == 0, !.
simp(A&B, B) :- A == 1, !.
simp(A&B, A) :- B == 1, !.
simp(A '|' B, B) :- A == 0, !.
simp(A '|' B, A) :- B == 0, !.
simp(A '|'_, 1) :- A == 1, !.
simp(_ '|' B, 1) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).


unsat(A) :- eval(A, B), term_variables(B, L), unsat(B, L).

unsat(0, _) :- !.
unsat(A, [0|_]) :- unsat(A), !.
unsat(A, [1|_]) :- unsat(A).

This prover is able to find quickly a counter-model for the following big disjunctive formula:

?- unsat((( A11 & A21 ) | ( ( A11 & A31 ) | ( ( A11 & A41 ) | ( ( A11 & A51 ) | ( ( A11 & A61 ) | ( ( A21 & A31 ) | ( ( A21 & A41 ) | ( ( A21 & A51 ) | ( ( A21 & A61 ) | ( ( A31 & A41 ) | ( ( A31 & A51 ) | ( ( A31 & A61 ) | ( ( A41 & A51 ) | ( ( A41 & A61 ) | ( ( A51 & A61 ) | ( ( A12 & A22 ) | ( ( A12 & A32 ) | ( ( A12 & A42 ) | ( ( A12 & A52 ) | ( ( A12 & A62 ) | ( ( A22 & A32 ) | ( ( A22 & A42 ) | ( ( A22 & A52 ) | ( ( A22 & A62 ) | ( ( A32 & A42 ) | ( ( A32 & A52 ) | ( ( A32 & A62 ) | ( ( A42 & A52 ) | ( ( A42 & A62 ) | ( ( A52 & A62 ) | ( ( A13 & A23 ) | ( ( A13 & A33 ) | ( ( A13 & A43 ) | ( ( A13 & A53 ) | ( ( A13 & A63 ) | ( ( A23 & A33 ) | ( ( A23 & A43 ) | ( ( A23 & A53 ) | ( ( A23 & A63 ) | ( ( A33 & A43 ) | ( ( A33 & A53 ) | ( ( A33 & A63 ) | ( ( A43 & A53 ) | ( ( A43 & A63 ) | ( ( A53 & A63 ) | ( ( A14 & A24 ) | ( ( A14 & A34 ) | ( ( A14 & A44 ) | ( ( A14 & A54 ) | ( ( A14 & A64 ) | ( ( A24 & A34 ) | ( ( A24 & A44 ) | ( ( A24 & A54 ) | ( ( A24 & A64 ) | ( ( A34 & A44 ) | ( ( A34 & A54 ) | ( ( A34 & A64 ) | ( ( A44 & A54 ) | ( ( A44 & A64 ) | ( ( A54 & A64 ) | ( ( A15 & A25 ) | ( ( A15 & A35 ) | ( ( A15 & A45 ) | ( ( A15 & A55 ) | ( ( A15 & A65 ) | ( ( A25 & A35 ) | ( ( A25 & A45 ) | ( ( A25 & A55 ) | ( ( A25 & A65 ) | ( ( A35 & A45 ) | ( ( A35 & A55 ) | ( ( A35 & A65 ) | ( ( A45 & A55 ) | ( ( A45 & A65 ) | ( A55 & A65 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )).
A11 = A21, A21 = A31, A31 = A41, A41 = A51, A51 = A12, A12 = A22, A22 = A32, A32 = A42, A42 = A52, A52 = A13, A13 = A23, A23 = A33, A33 = A43, A43 = A53, A53 = A14, A14 = A24, A24 = A34, A34 = A44, A44 = A54, A54 = A15, A15 = A25, A25 = A35, A35 = A45, A45 = A55, A55 = 0.
1 Like

Thanks, I did not notice the differences in the year.

I also liked your answer at SO, but there has to be a way to change the operators to the standard. I understand what you noted about | but there has to be some way to use the operators and get the code to work. Not something I have time for at the moment but something I do need to understand.

Now you see why I much prefer being here at the SWI-Prolog forum than using StackOverflow. :slightly_smiling_face:

1 Like

Please do not change ! to ‘|’. It wont work in ISO compatible Prolog systems, where op(1100, xfy, ‘|’) would fail. Also this here is not compatible:

simp(A '|' B, B) :- A == 0, !.

Many Prolog systems require this here, since operator priority is above 900. Thats why I lowered all priorities. You can check Tau Prolog:

simp((A '|' B), B) :- A == 0, !.

See here, Tau Prolog lifted the operator change restriction, but still requires parenthesis, as most Prolog systems originally do:

Same problem with GNU Prolog, never had the operator change restriction, but still requires parenthesis, as most Prolog systems originally do:

SWI-Prolog discourse is ok to post the SWI-Prolog dialect. On StackOverflow I try to post more portable Prolog code. Mainly oriented towards the ISO core standard.

Thanks for this instructive remark. I apologize for this change.
I was inspired by Jen’s Otten provers. See for example this interesting webpage:
http://www.jens-otten.de/tutorial_tableaux19/

Your attention to provide Prolog code mainly oriented towards the ISO standard is understandable and welcome, of course. Nevertheless, after the test I just did, I confirm that this ISO standard version with ! standing for the alternation connective fails with the big disjunctive formula but succeed with the ’ | ’ version. Of course, I am unable to explain why.

The ! works fine. If it doesn’t work you can raise a ticket for the
corresponding Prolog system, where there is problem. In GitHub
issues, or whatever ticket system the Prolog system has,

you can also post very long strings. You can use higher operator
priority, but its harder to write portable code. If you use lower operator
priority you are in the camp of bitwise operatios:

:- op(500, yfx, \/). 
:- op(500, yfx, /\). /* would prefer 400 here */
:- op(200, fy, \). /* would prefer 300 here */

And in the camp of CLP(B):

:- use_module(library(clpb)).

:-op(500, yfx, +).
:-op(400, yfx, *).
:-op(300, fy, ~).

Thanks again ! The trouble is that these operator symbols are not those of ILTP Library . It is a pity that the community of logicians and computer scientist has until now been unable to define standards universally accepted for this very small list of logical symbols… :frowning:

Here is the SWI-Prolog version that I am using, that is more recent than the version in Debian (Buster):
joseph@mx:~$ swipl --version
SWI-Prolog version 8.3.3 for x86_64-linux

Some of these systems don’t use ‘|’ for disjunction. They might typically
use v for disjunction. This is just the letter v, nothing more or less.
Its very readable:

[eclipse 3]: prove((p v (~q & r) -> (p v ~q) & (p v r)) , Result).

The Problem is in some Prolog systems ‘|’ has a special meaning.
Some Prolog system even rewrite ‘|’ into ‘;’.

Ulrich Neumerkel tried to ban ‘|’ in Corrigendum 2 of the ISO core
standard. I am not happy how he did it, but its a good advice

to refrain from using it.

I agree with you that v is much better than | to stand for disjunction. Unfortunately, many programmers and logicians have used the latter in some provers and some papers.

I realize that I have forgotten to congratulate for your Prolog program that is very concise and very elegant. I am much impressed.

Could you please post your alledged ! problem. I am really currious
whats going on. Could you please post it here:

https://github.com/jburse/jekejeke-devel/issues/43

Just post the offending code and example, together with the Prolog version you used into a fresh comment field. Maybe we can find an explanation for what is going wrong?

I am very confused and sorry. The problem was mine: just ONE | was not changed into ! and that explains the “false” output… SORRY ! I apologize.

Ok, then I can close the GitHub issue. Great, Thanks!