Implementing Quine's algorithm

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

40

@j4n_bur53 Here is the comparison, and maybe an unexpected result:

LP(B) with the big disunctive formula:

% 144,793 inferences, 0.017 CPU in 0.017 seconds (100% CPU, 8376493 Lips)

Your prover, with the exactly same formula:

 6,026 inferences, 0.002 CPU in 0.002 seconds (100% CPU, 2679674 Lips)

Your prover is the winner ! (If I read correctly these results).

42

You do not want to be the winner? :slight_smile:

45

I am afraid that I am not competent enough to provide the least help, but I am happy that my question led you to write this SAT solver à la Quine.
From a philosophical point of view, I dislike the word “Description Logic”, I do not mean that I dislike the theory, but the use of word “logic” to refer to a theory that is, in my opinion, closer to set theory than first order logic. On this philosophical point, Quine’s position is convincing: by contrast with FOL, set theory is not ontologically neutral and it seems to me that any “Description Logic” provides also an ontology. Logic stricto sensu is “the science of arguments”, and it does not worry about how is the world. But this was only a philosophical remark.

47

Thanks. The least what it can be expected from us is honesty. By “set theory” I did not mean what we need usually to get a language encoding mathematical theories, but only the concepts of set, parts, inclusion, etc. that seem to be used in the example given of a DL. That’s it.

49

You are certainly right. I do not know this sort of logic. Do you think it is a useful logic? I presume that you do.

51

It might be interesting to know how a SAT solver such as MiniSat fares in comparison with pure Prolog implementations. It seems MiniSat can be run from Prolog, using this package.

53

Thanks again. It is very interesting. Your culture in the history of Logic is very good also ! (By the way, did you receive the message I sent to you this morning? I loosed its trace.)

55

En français: GÉNIAL !
Thanks for this code !

56

I would be glad to get a method to implement pretty-print printers for these provers, like did Naoyuki Tamura here : http://bach.istc.kobe-u.ac.jp/seqprover/ is there a text book to learn how to do it?

59

Thanks Jan. That’s very nice! I did not know sandbox, I only heard about it. I am going to see that.

60

I just tested tau-prolog with sandbox, and it is really impressive. It can be very useful to help understand how Prolog computes. Thanks !

64

Hello, I reproduce here Isabelle Newbie’s program, with minor changes that allow a first improvement of the output:

% :- use_module(library(clpb)).
% :- use_module(library(check)).
% :- set_prolog_flag(stack_limit, 2_147_483_648).

:- op( 300, fy, ~).     % negation
:- op(400, xfy, &).    % conjunction
:- op(500, xfy, v).  % disjunction
:- op(600, xfy, =>).   % conditional
:- op(700, xfy, <=>).   % biconditional

formula_simpler(~ ~ P ,      P).
formula_simpler(~ ⊥,       ⊤).
formula_simpler(~ ⊤,       ⊥).
formula_simpler(_P & ⊥,   ⊥).
formula_simpler(⊥ & _P,   ⊥).
formula_simpler(P & ⊤,    P).
formula_simpler(⊤ & P,    P).
formula_simpler(P v ⊥,  P).
formula_simpler(⊥ v P,  P).
formula_simpler(_P v ⊤, ⊤).
formula_simpler(⊤ v _P, ⊤).
formula_simpler(P => ⊥,   ~ P).
formula_simpler(_P => ⊤,  ⊤).
formula_simpler(⊥ => _P,  ⊤).
formula_simpler(⊤ => P,   P).
formula_simpler(P <=> ⊥,  ~ P).
formula_simpler(⊥ <=> P,  ~ P).
formula_simpler(P <=> ⊤,  P).
formula_simpler(⊤ <=> P,  P).
formula_simpler(P <=> P, ⊤).

formula_simple2(Formula, Simple) :-
    Formula =.. [Operator | Args],
    maplist(formula_simple2, Args, SimpleArgs),
    SimplerFormula =.. [Operator | SimpleArgs],
    formula_rootsimple(SimplerFormula, Simple).

formula_rootsimple(Formula, Simple) :-
    (   formula_simpler(Formula, Simpler)
    ->  formula_rootsimple(Simpler, Simple)
    ;   Simple = Formula ).


formula_variable(Variable, Variable) :-
    atom(Variable),
    dif(Variable, ⊤),!,
    atom(Variable),
    dif(Variable, ⊥).
formula_variable(Formula, Variable) :-
    Formula =.. [_Operator | Args],
    member(Arg, Args),
    formula_variable(Arg, Variable),!.





variable_replacement_formula_replaced(Variable, Replacement, Variable, Replacement).
variable_replacement_formula_replaced(Variable, _Replacement, Formula, Formula) :-
    atom(Formula),
    dif(Formula, Variable).
variable_replacement_formula_replaced(Variable, Replacement, Formula, Replaced) :-
    Formula =.. [Operator | Args],
    Args = [_ | _],
    maplist(variable_replacement_formula_replaced(Variable, Replacement), Args, ReplacedArgs),
    Replaced =.. [Operator | ReplacedArgs].

quine(Formula) :-
    formula_simple2(Formula, ⊤),
    write(⊤),!.
quine(Formula) :-
    formula_simple2(Formula, SimpleFormula),
    formula_variable(SimpleFormula, Variable),
    !,
    variable_replacement_formula_replaced(Variable, ⊤, Formula, TopFormula),nl,
    write('Let us replace  '),write(Variable),write('  by ⊤ :'),nl,
    write(TopFormula),nl,
    quine(TopFormula),
    variable_replacement_formula_replaced(Variable, ⊥, Formula, BotFormula),
    nl,nl,write('Let us replace  '),write(Variable),write('  by ⊥ :'),nl,
    write(BotFormula),nl,
    quine(BotFormula).

Example of output:

?- quine(((p v q) => r) <=> ((p => r) & (q => r))).

Let us replace  p  by ⊤ :
⊤v q=>r<=>(⊤ => r)&(q=>r)

Let us replace  r  by ⊤ :
⊤v q=> ⊤ <=> (⊤ => ⊤)&(q=> ⊤)
⊤

Let us replace  r  by ⊥ :
⊤v q=> ⊥ <=> (⊤ => ⊥)&(q=> ⊥)
⊤

Let us replace  p  by ⊥ :
⊥v q=>r<=>(⊥ => r)&(q=>r)
⊤
true

Comment:

It is not still an exact translation of Quine’s algorithm, because it should have been this one:

?- quine(((p v q) => r) <=> ((p => r) & (q => r))).

Let us replace  p  by ⊤ :
⊤v q=>r<=>(⊤ => r)&(q=>r)
(T => r) <=> r & (q => r)
       r <=> r  & (q => r)  % Note: neither ⊥ nor T in the reduced formula
                            % therefore, new assignment in a new double
                            % table as follows:          

Let us replace  r  by ⊤ :
 ⊤ <=> T &(q=> ⊤)
 ⊤ <=> T & T
 T <=> T
    T

Let us replace  r  by ⊥ :
       r <=> r  & (q => r)
       ⊥ <=> ⊥  & (q => ⊥)
       ⊥ <=> ⊥
          T

Let us replace  p  by ⊥ :
⊥v q=>r<=>(⊥ => r)&(q=>r)
  (q => r) <=> T  & (q => r)
    (q => r) <=> (q => r)
              T
true

I would be surprised if this exact translation of Quine’s algorithm could not be given by another improvement of Isabelle Newbie program. But I do not know how to dot it. (Again, the interest of such a program is mainly pedagogical.

67

Thank you very much Jan for these helpful and very interesting answers.
Two points before trying again to improve the output details of the Quine program.
First, I explain why such a program would be educational: many students are now alone in front of their computers, if they can use a program that shows us in detail how to get a Quine proof or a Quine counter-model for any propositional formula, it might be useful to them. This brings me to the second point.
It is interesting to note that Quine’s algorithm and Beth’s algorithm (the tree method) have opposite directions: the former goes from the inside out, the latter the reverse, via the negation of the formula submitted to test. Maybe the solution would be to write a program that makes exactly what is to do with Quine’s algorithm: pick an atomic formula (if possible the most common in the formula), replace it by T, and apply the reduction rules from subformulas to subformulas until to be at the level of the main connective, and again make the same thing with replacing the same starting atom by ⊥ . I note that there is no use of predicate subformula in Isabelle Newbie program, and the solution is adding rules for subformulas? I do not know, I am too weak in Prolog. Again, my warmest regards.

69

I just tested your Boole program that is very interesting for me, because both it solves my problem and it is the most efficient. But I do not succeed to print the output of prove as you do, I’m using SWI-Prolog.

71

I see no prove predicate https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-boole-pl , I added it from your remarks, and I added also

prove(A) :- current_prolog_flag(sys_print_map, N), 
     write_term(A, [variable_names(N)]), nl, 
     eval(A, B), term_variables(B, L), prove(B, L).

Unfortunately, I do not get the print. Probably I missed something.