Thanks. My interest was only in the Prolog code to built for example Weakening on the left in L&, or Weaking on the right in Rv .
Yes. I got it. But the add of & on the left is a Weakening disguised, idem for the disjunction on the right, and I do not succeed to make it.
I do not doubt that you are right. I will trying to use your work to run this fork only with SWI-Prolog and your pretty-printer. I hope that I will be able to do it.
I do not see this link. 
Good news. I was just able to use your full program with latexer in my emacs:
?- prove0((a => a), []).
\begin{prooftree}\RightLabel{$ax$} \AxiomC{} \UnaryInfC{$a \vdash a$}\RightLabel{$R\!\!\!\implies$} \UnaryInfC{$ \vdash a \implies a$}\end{prooftree}
true.
Now, it should be possible to capitalize the propositional variables, how?
Latex commands \uppercase and \MakeUppercase should work … and indeed, it works. Solved.
I come back to my initial question. I have understood that with
provable(('P' => 'P'), Proof).
I get the output
rcond([]>[(P=>P)],ax([P]>[P],P))
But from the point of view of the user of a theorem prover, it is very tedious and source of errors. I’m trying desperately to find some lines of Prolog code in order to have as input
provable((p => p), Proof).
and nevertheless getting the same output i.e. with upper case atoms.
Thanks, but I do not have access to a program via your link.
It’s irritating that getting uppercase output for a theorem prover in Prolog seems to be so difficult. 
I remember by contrast the magic .toUpperCase(); in javascript…
Other sad point: I do not find a clear HowTo in order to learn pretty printing in Prolog. Nothing on this topic, except some programs online…
I have not followed all the complex details in this thread, but if your problem is just to transform of some parts of a term, seems you could use (for instance) string_upper/2 in a standard recursive visit of the term (that is, decompose and rebuild using =…/2), or the new mapargs/3 .
With this last
term_lower_upper(Lower,Upper) :-
mapargs(string_upper,Lower,Upper).
?- term_lower_upper(p(a,b,c),U),writeln(U).
p(A,B,C)
U = p("A", "B", "C").
But maybe I misunderstood the problem…
Thanks, Carlo.
Today I just succeed to get the half that I want., writing:
prove(G>D, rcond(G>D,P)):-
select((A=>B),D,D1),!,
upcase_atom(A,A1),
upcase_atom(B,B1),
prove([A1|G]>[B1|D1],P).
with the input
?- provable((a => a), Proof).
I get the output:
Prolog output : rcond([]>[(a=>a)],ax([A]>[A],A))
\begin{prooftree}\RightLabel{$\scriptsize{Ax.}$} \AxiomC{} \UnaryInfC{$ A \vdash A $}\RightLabel{$\scriptsize{R\to}$} \UnaryInfC{$ \vdash a \to a $}\end{prooftree}
true
and I do not succeed to go inside the molecular formula a => a to
“upcase” atom a.
I would avoid to change prove/2… instead, transform at once after prove/2 succeeded…
term_lower_upper(Lower,Upper) :-
( compound(Lower)
-> mapargs(term_lower_upper,Lower,Upper)
; is_list(Lower)
-> maplist(term_lower_upper,Lower,Upper)
; atomic(Lower) % this should be useless, but let's throw an exception just in case...
-> upcase_atom(Lower,Upper)
; throw(term_lower_upper(Lower,Upper))
).
?- term_lower_upper(p(a,b,[c,d>b,e]),U),writeln(U).
p(A,B,[C,D>B,E])
U = p('A', 'B', ['C', 'D'>'B', 'E']).
1 Like
Thanks Carlo. I see also j4n_bur53’s message. I am going to test these solutions. I’ll keep you informed.
Thanks @j4n_bur53 ! I need to learn DCG syntax…
Many thanks Carlo for this very elegant solution. It works perfectly inside @j4n_bur53 latexer.p (pretty printer for LaTeX). I wrote provable predicate as folllows:
% -----------------------------------------------------------------
provable(F,W):-
time(prove([]>[F],P)),
term_lower_upper(P,V),
nl,
write('Prolog output : '), write(P),
nl,
nl,
latex(V,W).
% -----------------------------------------------------------------
with adding you code at the end of the prolog prover, before the petty-printer and now:
?- provable((p => p), Proof).
% 10 inferences, 0.000 CPU in 0.000 seconds (95% CPU, 144776 Lips)
Prolog output : rcond([]>[(p=>p)],ax([p]>[p],p))
\begin{prooftree}\RightLabel{$\scriptsize{Ax.}$} \AxiomC{} \UnaryInfC{$ P \vdash P $}\RightLabel{$\scriptsize{R\to}$} \UnaryInfC{$ \vdash P \to P $}\end{prooftree}
true
Congratulations. That is very nice.
It should be impossible in theory, because F.O. predicate calculus is semi-decidable, by contrast with its propositional calculus part which is decidable. In my opinion, you know better than me that the explanation of this fact lies in Löwenheim-Skolem theorems, irrelevant to this forum. Thanks for having pointed out to me this point with your Socratic question.
An excellent book, indeed.
Thanks, because indeed, it seems to be a real improvement on efficiency, at least for some formulas:
For Pelletier problem 17, with your leantap code:
% 236 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 502667 Lips)
with leanseq now:
% 891 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 2262915 Lips)
But this leantap fails to prove Pelletier problem 71,
% 85,505,302 inferences, 11.798 CPU in 11.799 seconds (100% CPU, 7247370 Lips)
ERROR: Stack limit (1.0Gb) exceeded
ERROR: Stack sizes: local: 3Kb, global: 0.9Gb, trail: 25.9Mb
ERROR: Stack depth: 54, last-call: 54%, Choice points: 6
ERROR: In:
ERROR: [54] user:prove(<compound (>)/2>, <compound lbicond/3>)
ERROR: [52] user:prove(<compound (>)/2>, <compound lbicond/3>)
ERROR: [50] user:prove(<compound (>)/2>, <compound lbicond/3>)
ERROR: [48] user:prove(<compound (>)/2>, <compound lbicond/3>)
ERROR: [46] user:prove(<compound (>)/2>, <compound lbicond/3>)
a formula provable with this fork of leanseq.pl . The failure seems to be caused by the left biconditionnal rule.
I will have a closer look on this point later on (but maybe the removal of the deterministic select/3 could be finally a bad thing?)
Very impressive. Congratulations !
It is not my system, but only small changes from Zucker-Otten’s program. You just proved that there is still more efficient. Congrats again.