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

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.

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.

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!

Yes, but as noted

and the reason the teacher introduced it in the class is that it makes for an example that has enough meat on the bone to learn from and not so much as to drown the student.

In the land of parsing and evaluation examples, I have seen so many examples of basic parsing and evaluation for addition and subtraction that if I were to teach a class on basic parsing and evaluation I would not use addition and subtraction as there are so many examples it would be hard to identify if the student copied it or created it. For now implementations of Quine’s Algorithm are hard to find and thus useful for teaching. Also because it uses boolean logic and not math, many students would have to think about what they are writing instead of mindless writing code that doesn’t really help them learn.

1 Like

That’s indeed very interesting. I will compare with CLP(B).

Complexity theory has also its pedagogy. Do you imply that teaching should be void of complexity considerations. pedagogical could mean simple without too much distracting technical details. This doesn’t necessarely exclude showing complexity behaviour.