Interesting. Congratulations for Jekejeke Prolog ! I am going to see for sys_print_map flag with SWI.
In the long list that is the output of
?- current_prolog_flag(X, Y), write(X-Y), nl, fail; true.
I see :
print_write_options-[portray(true),quoted(true),numbervars(true)]
is it the useful code to get the print of proofs?
I am lost with printing in Prolog…
?- read_term(A, [variable_names(N)]).
|: |: prove(((P v Q) => R) <=> ((P => R) & (Q => R))).
A = prove(_4916 v _4918=>_4924<=>(_4916=>_4924)&(_4918=>_4924)),
N = ['P'=_4916, 'Q'=_4918, 'R'=_4924].
That’s it.
I confess I do not understand all.
The sad thing is that I remain unable to get what you got with your Prolog, that is this output:
?- prove(((P+Q)=<R)=:=((P=<R)*(Q=<R))).
(P+Q =< R) =:= (P =< R)*(Q =< R)
(0+Q =< R) =:= (0 =< R)*(Q =< R)
(0 =< R) =:= (0 =< R)
(1 =< R) =:= (1 =< R)
0 =:= 0
1 =:= 1
(1+Q =< R) =:= (1 =< R)*(Q =< R)
0 =:= 0*(Q =< 0)
1 =:= 1*(Q =< 1)
Yes /* Proof Complete */
It is my main concern at the moment: to get a printed proof from Quine program. And I must tell that I am unable to find a clear documentation on the web how to define a pretty printing with SWI-Prolog, the official documentation is too much cryptic for my small brain… 
Nothing works with my SWI-Prolog, but maybe the problem is in my file. Could you put your complete file somewhere to leave me able to test it with my Prolog, please?
With my file (that contains other usual symbols as operators), I get the following input:
?- taut(((A v B) => C) <=> ((A => C) & (B => C)), T).
A = C, C = T, T = 1
?- taut(~ A v A, S).
A = S, S = 1
That is correct but very different, because the truth value analysis is not given.
With this code:
taut(T, [], T) :- !.
taut(A, [B|_], T) :- catch((B = 0, taut(A, T), throw(T)), T, true),
B = 1, taut(A, S), T = S.
% taut(A, T) :- eval(A, B), term_variables(B, L), taut(B, L, T).
taut(A, T) :-
eval(A, B),
current_prolog_flag(sys_print_map, N),
write_term(A, [variable_names(N)]),
write(' --> '),
write_term(B, [variable_names(N)]),nl,
term_variables(B, L),
taut(B, L, T).
I get this output:
?- taut(((A v B) => C) <=> ((A => C) & (B => C)), T).
false.
And with this one:
taut(T, [], T) :- !.
taut(A, [B|_], T) :- catch((B = 0, taut(A, T), throw(T)), T, true),
B = 1, taut(A, S), T = S.
% taut(A, T) :- eval(A, B), term_variables(B, L), taut(B, L, T).
taut(A, T) :-
eval(A, B),
% current_prolog_flag(sys_print_map, N),
write_term(A, [variable_names(N)]),
write(' --> '),
write_term(B, [variable_names(N)]),nl,
term_variables(B, L),
taut(B, L, T).
I get :
?- taut(((A v B) => C) <=> ((A => C) & (B => C)), T).
ERROR: Arguments are not sufficiently instantiated
ERROR: In:
ERROR: [11] write_term(... => _8954<=> ... & ...,[variable_names(_8970)])
ERROR: [10] taut(... => _9008<=> ... & ...,_8996) at /home/joseph/MEGA/projets/cours_prolog/boole2.pl:99
ERROR: [9] <user>
?-
I test this solution tomorrow and I’ll tell you. Many thanks !
Hello, I just made the test and it fails:
?- read_term(A, [variable_names(N)]), taut(A, T, N).
|: taut(B => B, T, N).
taut(B=>B,T,N) --> taut(B=>B,T,N)
taut(0=>0,T,N) --> taut(0=>0,T,N)
taut(0=>0,0,N) --> taut(0=>0,0,N)
taut(0=>0,0,0) --> taut(0=>0,0,0)
ERROR: Unhandled exception: taut(0=>0,0,0)
I am sorry.
Sorry, I misunderstood completely this point ! It works perfectly on my side also now:
?- read_term(A, [variable_names(N)]), taut(A, T, N).
|: A =< A.
A=<A --> A=<A
0=<0 --> 1
1=<1 --> 1
A = (1=<1),
N = ['A'=1],
T = 1.
And it is highly probable that it worked from the beginning with taut/2 .
I apologize, and I thank you warmly for your Prolog lessons.
I am going to send it a useful email to thank you as I have to dot it. 
I just remarked maybe the same point:
?- read_term(A, [variable_names(N)]), taut(A,T, N).
|: ~ (~ A + A).
~ (~A+A) --> ~ (~A+A)
~ (~0+0) --> 0
~ (~1+1) --> 0
A = ~ (~1+1),
N = ['A'=1],
T = 0.
Note that the result in the proof is in fact a tautology, not an antilogy.
More on this point. For convenience, on a file that takes the usual symbols for operators, I have written this code:
quine:-
getFormula(_A,_T).
getFormula(A,T):-
read_term(A, [variable_names(N)]), taut(A,T, N),nl,
write('Test successful. The formula is a tautology.'),nl,
quine,nl
;
falsify(A),nl,
write('Failure. The formula is not a tautology.'),nl,
quine.
Clearly, because CPL is decidable, any wff formula is valid or it is possible to provide a counter-model, hence the above disjunction. But with this code I get this:
?- quine.
|: (A => B) v (B => A).
(A=>B)v(B=>A) --> (A=>B)v(B=>A)
(0=>B)v(B=>0) --> 1
(1=>B)v(B=>1) --> 1
Test successful. The formula is a tautology.
|: ~ ((A => B) v (B => A)).
~ ((A=>B)v(B=>A)) --> ~ ((A=>B)v(B=>A))
~ ((0=>B)v(B=>0)) --> 0
~ ((1=>B)v(B=>1)) --> 0
Test successful. The formula is a tautology.
|: ~(~ A v A).
~ (~A v A) --> ~ (~A v A)
~ (~0 v 0) --> 0
~ (~1 v 1) --> 0
Test successful. The formula is a tautology.
Yes, you are right (as usually), but with my code “quine”, the output is not complete: T is not given, and I do not understand why…
You find the word “antilogical” in Quine’s correspondence here http://index-of.es/z0ro-Repository-3/Carnap/[Dear%20Carnap,%20Dear%20Van].pdf
Thanks for your solution, that works well, but I do not know how to write in Prolog this disjunction with three terms: T = 1 -> the formula is a tautology ; T = 0 the fomula is an antilogy ; the formula is neither a tautology nor an antilogy.
The following code fails and do not make the job:
getFormula(A,T):-
(read_term(A, [variable_names(N)]), taut(A,T, N),nl,
T = 1 -> write('The formula is a tautology.'),nl,
quine)
;
(T = 0 -> write('The formula is an antilogy.'),nl,
quine
;
falsify(A),nl,
write('The formula is neither a tautology nor an antilogy.'),nl,
quine).
because I get the following output:
?- quine.
|: (~ A v A) => (B & C).
~A v A=>B&C --> ~A v A=>B&C
~0 v 0=>B&C --> B&C
0&C --> 0
1&C --> C
0 --> 0
1 --> 1
The formula is an antilogy.
that is of course wrong.
It seems you might have gotten the parentheses or the conditional wrong here. If you indented it in a more usual way:
getFormula(A, T) :-
( read_term(A, [variable_names(N)]),
taut(A, T, N),
nl,
T=1
-> write('The formula is a tautology.'),
nl,
quine
; T=0
-> write('The formula is an antilogy.'),
nl,
quine
; falsify(A),
nl,
write('The formula is neither a tautology nor an antilogy.'),
nl,
quine
).
Is this what you meant to write?
If you want to have:
if Cond1 then Action1
else if Cond2 then Action2
else Action3
You would have to write:
( Cond1
-> Action1
; Cond2
-> Action2
; Action3
)
You could also try to avoid using = (unification) for comparison; use == (equivalence) instead, because:
?- T = 0.
T = 0. % the "true" is silent here
?- T == 0.
false.
Thanks for your help. The problem is to find a solution in this program to make the distinction between a formula that is simply satisifable (without being a tautology) and an antilogy… At the moment I do not find it.
I don’t claim to understand the full picture, but maybe you want:
getFormula(A, T) :-
read_term(A, [variable_names(N)]),
( taut(A, T, N),
nl,
( T==1
-> write('The formula is a tautology.'),
nl,
quine
; T==0
-> write('The formula is an antilogy.'),
nl,
quine
)
; falsify(A),
nl,
write('The formula is neither a tautology nor an antilogy.'),
nl,
quine
).
This mixing of logic and input/output always makes code structure more complicated than they need to be.
1 Like
Perfect ! You gave to me the right code:
?- quine.
|: A.
A --> A
0 --> 0
1 --> 1
The formula is neither a tautology nor an antilogy.
|: ~ (~ A v A).
~ (~A v A) --> ~ (~A v A)
~ (~0 v 0) --> 0
~ (~1 v 1) --> 0
The formula is an antilogy.
|: ~ A v A.
~A v A --> ~A v A
~0 v 0 --> 1
~1 v 1 --> 1
The formula is a tautology.
|:
THANKS !