Implementing Quine's algorithm

Help! Algorithm
1

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
2

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
3

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.

4

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.

6

Thanks for this clarification !

7

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
8

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.

9

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

1 Like
11

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/

12

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.

14

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:

16

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

18

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.

19

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

22

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.

24

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
25

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

27

In my opinion, no related topic should be a priori excluded, of course. But, for sure, there is a difference between applying correctly but blindly a method and understanding deeply why this method works. A lot of people (including me) start to be in the former situation, and when they are interested come gradually to the latter. Quine’s algorithm is an easy tool, as tree methods. Understanding them deeply is quite another thing. IMHO.

2 Likes
29

No, but you can’t toss a student into something that is so over their head that they lose interest in trying to solve the problem. This gives them a stepping stone to advance to harder problems.

As noted by the OP

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

Your code provides the answer to the OPs problem and is much cleaner than the answer by Isabelle Newbie and gives the details left out by the skeleton from jnmonette.

If one were to look at the more complex examples in the references I gave, they should see your implementation in their, or at least see the concepts. I did not check each to see how close they are to your answer but in having done many of these, they tend to refactor down to the same concept.

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

PRESS: PRolog Equation Solving System

1 Like
31

Some people can learn from an explanation, some need one example, some learn when seeing a spread of examples. Thee references give them that option.