Implementing Quine's algorithm

Help! Algorithm
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.

33

I did.

The way I read your post

is that you are saying that Quine’s Algorithm is of no value because it is not fast enough. I do not disagree with that.

What I am saying is that the value of Quine’s Algorithm is in teaching. I would not use it in a production environment but I would use it for teaching.

The original reason I was willing to add the 200 bounty points at SO was because I have seen lots of algorithms and methods in the area of logic simplification and automated theorem proving and did not recall seeing Quine’s Algorithm before. So I was thinking I might have missed something but in learning more came to realize that the value of Quine’s Algorithm is in teaching. Since it is not fast and efficient on real world problems it is not mentioned often.

35

I know it is the larger set of test cases, but I don’t know exactly where the OP is headed and giving him the page with more test that he can select from is easier than me spending repeated discussions of feeding them out one by one.

36

@j4n_bur53 At risk to appear stupid, I would be happy to get the complete translation of “unsat” in your program. If F is a tautology, unsat(F) fails. Interpreted naturally, it should not mean “unsatisfiable”: that is the negation of a tautology that is always false, i.e. unsatisfiable. What “unsat” means to you in your nice program?

37

Sorry. I realize that I give the reply in my own question. :frowning:

39

You are right and you explain also the difficulty that I felt confusedly.