How to use of upcase_atom/2 to get uppercase letters in an output

Help! Data Structure
1

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

the output for the example

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

is the following one:

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:

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.

3

Thanks . It works perfectly !

6

In Phil Zucker prover online, test the following formula:

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

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

10

I tried

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

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

13

See Render mathematical formulas

1 Like
15

@j4n_bur53 , yes, you suspected correctly that bussproofs.sty is translated only in MathJax 3.

18

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.

19

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.)

20

Thanks for reply.

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).

% ?- 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].

% ?- 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].
23

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.

24

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

25

“invalid” means simply “unprovable” and not “contradictory”. See for example the use of “invalid” here:
THE LOGIC NOTES. In other words, “invalid” means exactly “falsifiable”, that’s it.

26

I see. Thank you.

28

https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html

Just published on my personal blog.

2 Likes
30

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

33

About the failure of the prove function, I am indebted to the work of Enrico Tassi and Stefano Zacchiroli, see their prover for G3cp and G3 ip here :

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

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.

34

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.

35

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/

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}
}

I share this paper via my website:

https://www.vidal-rosset.net/pdf/dyckhoff92.pdf

It is easy to get Zucker’s page and all its code via GNU Wget and this command line:

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

Example :

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.)

38

Please, have a look on 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…

41

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

%% 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.