# How to use of upcase\_atom/2 to get uppercase letters in an output

**URL:** <https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693>\
**Category:** Data Structure\
**Tags:** how-to\
**Created:** [November 30, 2021, 12:46pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693 "2021-11-30T12:46:05Z")\
**Posts on this page:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [November 30, 2021, 12:46pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/1 "2021-11-30T12:46:05Z")

</div>

Hello,  
There is a nice theorem prover for propositional logic with LK implemented in Prolog here:

> **[Automated Propositional Sequent Proofs in Your Browser with Tau Prolog](https://www.philipzucker.com/javascript-automated-proving/)**
>
> Hot Leaves in a Cold Worlds.

the output for the example

```prolog
prove0(((a & b) => a), Proof). 

```

is the following one:

```prolog
Proof = rimpl([]>[(a&b=>a)],land([(a&b)]>[a],ax([a,b]>[a],a))).

```

I wonder how to capitalize the atoms to get from this second output instead of the first one:

```prolog
Proof = rimpl([]>[(A&B=>A)],land([(A&B)]>[B],ax([B,B]>[A],A))).

```

Because I guess that the image of the sequent proof wich is provided by the LateX macro bussproofs.sty implemented in MathJax would give variables in uppercase via the Tau Prolog script. Ido not doubt that such a program could also be written in SWI-Prolog, but I prefer to focus on the use of upcase\_atom/2 for this leanseq.pl program or on any lines of Prolog code to get propositional variables in uppercase.  
Thanks for your help or your suggestions !  
Jo.

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [November 30, 2021, 2:38pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/3 "2021-11-30T14:38:40Z")

</div>

Thanks . It works perfectly !

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 1, 2021, 1:58pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/6 "2021-12-01T13:58:06Z")

</div>

In Phil Zucker prover online, test the following formula:

```prolog
prove0(((A & B) => A), Proof). 

```

and you’ll see that, unfortunately, because of MathJax, it is not the solution.

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 4, 2021, 1:15pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/10 "2021-12-04T13:15:43Z")

</div>

I tried

```prolog
prove0((('A' & 'B') => 'A'), Proof).

```

and indeed, it works. Thanks for this Prolog lesson .

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [December 5, 2021, 5:40pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/13 "2021-12-05T17:40:15Z")

</div>

> [@anon95304481](#):
>
> Also nice MathJax dressing inside [SWISH](https://swish.swi-prolog.org/) would be cool.

See [Render mathematical formulas](https://swish.swi-prolog.org/example/render_mathjax.swinb)

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 6, 2021, 9:54pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/15 "2021-12-06T21:54:48Z")

</div>

@anon95304481 , yes, you suspected _correctly_ that bussproofs.sty is translated only in MathJax 3.

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [December 9, 2021, 10:54am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/18 "2021-12-09T10:54:37Z")

</div>

> [@joseph-vidal-rosset](#):
>
> [Automated Propositional Sequent Proofs in Your Browser with Tau Prolog | Hey There Buddo!](https://www.philipzucker.com/javascript-automated-proving/)

The following formula is the last of seven sample queries in the article. My recent experimental zdd based refutation prover says that it is not valid, e.g., falsifiable.

`(~b => f) & ((b & f) => ~i) & ((i | ~b) => ~f) => (i & f)`

If this is valid like the rest of the queries, I have to debug my codes, which might be highly probable, though. A simple calculation by hand also said it is not valid, so I am confused for now.

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 9, 2021, 11:18am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/19 "2021-12-09T11:18:20Z")

</div>

It is indeed an invalid formula and Otten’s prover on Zucker’s web page gives the result “failed to prove”. To give more details, the valuation _b = true_ and _i = false_ is enough to falsify this formula. (I have succeeded to improve this prover to provide immediately countermodels. I will publish this soon on my webpage.)

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [December 9, 2021, 11:35am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/20 "2021-12-09T11:35:04Z")

</div>

Thanks for reply.

> [@joseph-vidal-rosset](#):
>
> It is indeed an invalid formula

BTW, I was not sure at all on my calculation, so I called library(clpb) for help,  
which has made me at peace. (Thanks Triska.)

CORRECTION.

I had mistaken. The log below is that really obtained by running library(clpb).  
However, they seem to say that the proposition is both satisfiable and falsifiable,  
that is, neither valid nor invalid. Strange. Am I missing ? Also the zdd based prover  
of mine shows the same thing as library(clpb).

```prolog
% ?- Prop = ( (~(B) =< F) * ((B * F) =< ~(I)) * ((I + ~(B)) =< ~(F)) =< (I * F)),
%	term_variables(Prop, Vs),
%	sat(Prop), labeling(Vs).
%@ Prop = ((~(0)=<0)*(0*0=< ~(0))*(0+ ~(0)=< ~(0))=<0*0),
%@ B = F, F = I, I = 0,
%@ Vs = [0, 0, 0] ;
%@ Prop = ((~(0)=<0)*(0*0=< ~(1))*(1+ ~(0)=< ~(0))=<1*0),
%@ B = F, F = 0,
%@ I = 1,
%@ Vs = [0, 0, 1] ;
%@ Prop = ((~(0)=<1)*(0*1=< ~(0))*(0+ ~(0)=< ~(1))=<0*1),
%@ B = I, I = 0,
%@ F = 1,
%@ Vs = [0, 1, 0] ;
%@ Prop = ((~(0)=<1)*(0*1=< ~(1))*(1+ ~(0)=< ~(1))=<1*1),
%@ B = 0,
%@ F = I, I = 1,
%@ Vs = [0, 1, 1] ;
%@ Prop = ((~(1)=<1)*(1*1=< ~(1))*(1+ ~(1)=< ~(1))=<1*1),
%@ B = F, F = I, I = 1,
%@ Vs = [1, 1, 1].

```

```prolog
% ?- Prop = ( (~(B) =< F) * ((B * F) =< ~(I)) * ((I + ~(B)) =< ~(F)) =< (I * F)),
%	term_variables(Prop, Vs),
%	sat(~Prop), labeling(Vs).
%@ Prop = ((~(1)=<0)*(1*0=< ~(0))*(0+ ~(1)=< ~(0))=<0*0),
%@ B = 1,
%@ F = I, I = 0,
%@ Vs = [1, 0, 0] ;
%@ Prop = ((~(1)=<0)*(1*0=< ~(1))*(1+ ~(1)=< ~(0))=<1*0),
%@ B = I, I = 1,
%@ F = 0,
%@ Vs = [1, 0, 1] ;
%@ Prop = ((~(1)=<1)*(1*1=< ~(0))*(0+ ~(1)=< ~(1))=<0*1),
%@ B = F, F = 1,
%@ I = 0,
%@ Vs = [1, 1, 0].

```

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [December 10, 2021, 2:35am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/23 "2021-12-10T02:35:38Z")

</div>

My concern was: whether a specific proposition is satsifiable or not,  
which may require, depending on the result, more debug on my codes on the prover. Now I have realized that my post is too personal, something off the line of discussion in this thread, perhaps which is related to categoricity of logics, which is too hard for me.

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [December 10, 2021, 4:44am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/24 "2021-12-10T04:44:40Z")

</div>

> [@anon95304481](#):
>
> empty

The empty set is a function by definition of the function.,.

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 10, 2021, 8:20am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/25 "2021-12-10T08:20:31Z")

</div>

> [@kuniaki.mukai](#):
>
> I had mistaken. The log below is that really obtained by running library(clpb).  
> However, they seem to say that the proposition is both satisfiable and falsifiable,  
> that is, neither valid nor invalid.

“invalid” means simply “unprovable” and not “contradictory”. See for example the use of “invalid” here:  
[THE LOGIC NOTES](https://users.cecs.anu.edu.au/~jks/LogicNotes/soundness-and-completeness.html). In other words, “invalid” means exactly “falsifiable”, that’s it.

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [December 10, 2021, 11:08am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/26 "2021-12-10T11:08:33Z")

</div>

> [@joseph-vidal-rosset](#):
>
> “invalid” means simply “unprovable” and not “contradictory”.

I see. Thank you.

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 11, 2021, 8:07pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/28 "2021-12-11T20:07:51Z")

</div>

[https://www.vidal-rosset.net/sequent\_calculus\_prover\_with\_antisequents\_for\_classical\_propositional\_logic.html](https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html)

Just published on my personal blog.

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [December 12, 2021, 5:37am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/30 "2021-12-12T05:37:44Z")

</div>

I remember that once long time ago, I wrote a swi-prolog cgi page for propositional LK calculus before at least 2006. It displays a text based proof figure, not in LaTex. More worse, it is in Japanese. It is a simple minded prover as an exercise on AJax. I am afraid there is nothing interest for you, but it is surprising for me that the CGI still works !

[http://web.sfc.keio.ac.jp/~mukai/paccgi7/gentzen.html](http://web.sfc.keio.ac.jp/~mukai/paccgi7/gentzen.html)

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 12, 2021, 9:56am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/33 "2021-12-12T09:56:22Z")

</div>

About the failure of the prove function, I am indebted to the work of [Enrico Tassi](http://www.cs.unibo.it/~tassi) and [Stefano Zacchiroli](http://www.cs.unibo.it/~zacchiro), see their prover for G3cp and G3 ip here :

[https://www.vidal-rosset.net/g3cp-g3ip/](https://www.vidal-rosset.net/g3cp-g3ip/)

In my opinion, it is interesting to understand why because of the proof search in Prolog, the failure rule

```prolog
prove(G>D, asq(G<D, asq)):-
        \+ (member(A,G), member(A,D)).

```

must be at the last rule of this prover: all the previous rules for connectives have been used previously, the failure rules succeeding, the proof search stops, and the proof that is a refutation is done.

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 12, 2021, 10:05am UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/34 "2021-12-12T10:05:25Z")

</div>

I regret now that MathJax does not contain more proof formats which are provided by LaTeX macros: the variety of styles for Natural Deduction for example. It would be possible the to construct from the same output Prolog differents styles of proofs (thanks to people better than me with code). This was the project of a website called “Proof Web”, but I do not know if it still works.

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 12, 2021, 12:32pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/35 "2021-12-12T12:32:02Z")

</div>

I already “forked” Naoyuki Tamura’s prover to make a G4i prover and I  
tried to get a classical G4 prover, with hoping that this latter is correct.

[https://www.vidal-rosset.net/g4-prover/](https://www.vidal-rosset.net/g4-prover/)

I don’t know if an implementation of LJ exists in a prover. Dyckhoff  
published his famous paper on LJT (i.e. G4i) that is LJ “terminating”,  
where he mentioned at the beginning LJ loops. If an LJ prover is  
nevertheless possible, it should be published.

@Article{dyckhoff92,  
Title = {{Contraction-Free Sequent Calculi for  
Intuitionistic Logic}},  
Author = {Dyckhoff, R.},  
Journal = {Journal of Symbolic Logic},  
Year = {1992},  
Number = {3},  
Pages = {795-807},  
Volume = {57},  
doi = {10.2307/2275431},  
url = {[Contraction-Free Sequent Calculi for Intuitionistic Logic on JSTOR](https://www.jstor.org/stable/2275431)}  
}

I share this paper via my website:

[https://www.vidal-rosset.net/pdf/dyckhoff92.pdf](https://www.vidal-rosset.net/pdf/dyckhoff92.pdf)

> [@anon95304481](#):
>
> The problem I cannot directly enter visualizations Phil  
> Zuckers page.

It is easy to get Zucker’s page and all its code via [GNU Wget](https://www.gnu.org/software/wget/) and this command line:

```prolog
wget -r -k -np --user-agent=Firefox url-of-the-website

```

Example :

```prolog
joseph@mx:~/src$ wget -r -k -np --user-agent=Firefox https://www.philipzucker.com/javascript-automated-proving/
--2021-12-12 13:39:27-- https://www.philipzucker.com/javascript-automated-proving/
Résolution de www.philipzucker.com (www.philipzucker.com)… 2606:50c0:8001::153, 2606:50c0:8000::153, 2606:50c0:8003::153, ...
Connexion à www.philipzucker.com (www.philipzucker.com)|2606:50c0:8001::153|:443… connecté.
requête HTTP transmise, en attente de la réponse… 200 OK
Taille : 45997 (45K) [text/html]
Sauvegarde en : « www.philipzucker.com/javascript-automated-proving/index.html »

www.philipzucker.com/jav 100%[==================================>] 44,92K --.-KB/s ds 0,002s  

2021-12-12 13:39:27 (19,6 MB/s) — « www.philipzucker.com/javascript-automated-proving/index.html » sauvegardé [45997/45997]

Terminé — 2021-12-12 13:39:27 —
Temps total effectif : 0,2s
Téléchargés : 1 fichiers, 45K en 0,002s (19,6 MB/s)
Conversion des liens de www.philipzucker.com/javascript-automated-proving/index.html… 7.
2-5
Liens convertis dans 1 fichiers en 0,002 secondes.

```

(This command does not work for my own website which is probably protected more that I wish. Hence the links to get the source files.)

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 13, 2021, 1:41pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/38 "2021-12-13T13:41:43Z")

</div>

> [@anon95304481](#):
>
> What makes you think MathJax cannot display natural deduction?

Please, have a look on [BussGuide2.pdf](https://ctan.mines-albi.fr/macros/latex/contrib/bussproofs/BussGuide2.pdf). You’ll see that MathJax display just a part of what can be done in LaTeX via bussproofs.sty Of course, natural deduction in sequent style can be displayed by MathJax 3 via bussproofs module, but I do not think that Mathjax displays for example natural deduction in Fitch style (i.e. “flag style”). More generally, there are a lot of LaTeX macros for logical proofs, and very few are displayed by MathJax (in fact I know only bussproofs which, fortunately, is in this case). It is not a criticism, but just a fact, I guess that it is a lot of work…

---

<div class="post-metadata">

**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [December 15, 2021, 1:17pm UTC](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/41 "2021-12-15T13:17:47Z")

</div>

> [@anon95304481](#):
>
> What about this riddle

I’m trying to translate the rule for conditional elmination in Jens Otten code, to get natural deduction in sequent style, but until now, all my tentative failed. I’m starting to doubt that it is possible to use the same predicates of this code for the left conditional rule in LK

```prolog
%% 9. conditional on the left
prove(G>D, lcond(G>D,P1,P2)):-
        select((A=>B),G,G1),!,
        prove(G1>[A|D],P1),
        prove([B|G1]>D,P2).

```

to get the conditional elimation rule of natural deduction … If the solution exists, I did not see it.

[Next page](https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693.md?page=2)