SWI-Prolog - PHP - Html

Hello.
I would be glad to publish the prover below online, to be used online on my website. The simplest way would be the best, but I need clear and complete explanations. Thanks !

/*
This prover is the work of Jan Burse. I changed only the symbols for operators, that's it.
See the web page : https://swi-prolog.discourse.group/t/implementing-quines-algorithm/2830
and also https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in?noredirect=1#comment112667699_63505466
the boole.pl original file is here: https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-boole-pl
*/
:- use_module(library(statistics)).

:- op(700, xfy, <=>).
:- op(600, xfy, =>).
:- op(500, xfy, v).
:- op(400, xfy, &).
:- op(300, fy, ~).

eval(A, A) :- var(A), !.
eval(A => B, R) :- !, eval(A, X), eval(B, Y), simp(X => Y, R).
eval(A <=> B, R) :- !, eval(A, X), eval(B, Y), simp(X <=> Y, R).
eval(A v B, R) :- !, eval(A, X), eval(B, Y), simp(X v Y, R).
eval(A & B, R) :- !, eval(A, X), eval(B, Y), simp(X & Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).

simp(A, A) :- var(A), !.
simp(A => _, 1) :- A == 0, !.
simp(A => B, X) :- B == 0, !, simp(~A, X).
simp(A => B, B) :- A == 1, !.
simp(_ => B, 1) :- B == 1, !.
simp(A <=> B, X) :- A == 0, !, simp(~B, X).
simp(A <=> B, X) :- B == 0, !, simp(~A, X).
simp(A <=> B, B) :- A == 1, !.
simp(A <=> B, A) :- B == 1, !.
simp(A v B, B) :- A == 0, !.
simp(A v B, A) :- B == 0, !.
simp(A v _, 1) :- A == 1, !.
simp(_ v B, 1) :- B == 1, !.
simp(A & _, 0) :- A == 0, !.
simp(_ & B, 0) :- B == 0, !.
simp(A & B, B) :- A == 1, !.
simp(A & B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).

judge(A, [B|R]) :-
eval(A, B),
term_variables(B, L),
judge(B, L, R).

% Boole prover
% First, write "boole" + Enter.
% Second, write your formula + Enter.

judge(_, [], R) :- !, R = [].
judge(A, [B|L], R) :-
copy_term(A-[B|L], C-[0|L]),
copy_term(A-[B|L], D-[1|L]),
judge(C & D, R).

boole :-
get_wff(_A,_L).

get_wff(A,L) :-
time(judge(A,L)),
last(L,R),
(
last(L,1) ->  write('to prove that the formula is a tautology, i.e. that its truth value is always '),
write(R),write(' .'),nl,nl,nl,
boole
;

last(L,0) -> write('to prove that the formula is not a tautology, i.e. that its truth value can be '),
write(R),write(' .'),nl,nl,nl,
boole
).

% Second prover, Quine prover more practical and more verbose:
% First, write "quine" + Enter.
% Second, write only your formula + Enter.

taut(A, T, N) :-
eval(A, B),
write_term(A, [variable_names(N)]),nl,
write_term(B, [variable_names(N)]),nl,
write('------------------------------'),nl,
term_variables(B, L), taut(B, L, T, N),nl.

/*
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0,taut(A, T, N), throw(T)), T, true),
B = 1, write(N),nl,nl,taut(A, S, N), T = S.
*/

taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 1,write(N),write(':'),nl,nl,taut(A, T, N),throw(T)), T, true),
B = 0,
write(N),write(':'),nl,nl,
taut(A, S, N), T = S.

quine:-
getFormula(_A,_T).

getFormula(A, T) :-
(time(taut(A, T, N)) ->    /* here is the missing outer if-then-else */
(T == 1 ->
write('to prove that the formula is a tautology.'),
nl,nl,nl,
quine
;

write('to prove that the formula is an antilogy.'),
nl,nl,nl,
quine
)
;
write('to prove that the formula is neither a tautology nor an antilogy.'),
nl,nl,nl,
quine
).

2 Likes

Hi!

Thatâs a really cool thing

If the sandbox limitations of Swish allow it; this would be the simplest solution (in Swish you can preload a notebook with a git hub repo).

If swish does not work, i found this guide very useful!

Cheers/JC

1 Like

SWISH is probably not the solution:

No permission to call sandboxed `read_term(_1500,_1502)'
Reachable from:
getFormula(A,B)
quine

Therefore I am going to consult the guide to which you just referred. Thanks.

1 Like

SWISH would be a very nice solution. But it wonât be easy if you need to use term reading and writing for entering the formula.

Decoupling the reading and writing would altogether make it cleaner/easier to offer this functionality on a website.

Have you heard of code injection?

@Boris Never heard about code injection. In fact, I have already php files (not written by myself) that can give the result of input of another prover here . But, ironically, I do not succeed in getting the same result with this prolog program that is much simpler. I guess that webconsole.pl would be a solution.

Thanks Jan. I am happy if my difficulties can help to improve this nice tool that SWISH seems to be.

Hmm. It is not as easy as I thought. What does work though is using read_line_to_codes/2 and term_string/3, as in

term_string(Term, S, [variable_names(Names)]).

The price is that you must enter the formula on a single line.

Do not worry Jan. The work around is only to change the program in order to get a simple query that will work with SWISH. Now, I wonder if I can install SWISH into my website or if it is still better to save theses prolog provers on a SWISH instance somewhere else.
@j4n_bur53 It seems finally to me that the best is to publish these provers that are mainly the work of Jan Burse at http://lpsdemo.interprolog.com like I just did with unsat.pl that is the first program that Jan gave to me: http://lpsdemo.interprolog.com/p/unsat.pl But before going on I prefer to ask @j4n_bur53 his agreement.

Hacky but more efficient, as you know it.

I did it, and yesterday I changed the code in order to make it working with infix notation. I will publish it soon. It is a very good intuitionistic prover.

Thanks for this point. But I provided very little to your code Jan, my contribution is so weak that it seems to me that it is ridiculous to mention it. I will do it nevertheless, âtant pis pour le ridiculeâ. Thanks again for your precious help.

I will have a look on the licence issue. Thanks.

I got it. I will therefore publish the program that I adapted from Isabelle Newbieâs .

Very interesting. I have to learn how to do what you show to me.

@jan Is it possible for me to use the chat of SWISH with students who do not understand truth tables? I am searching something where I can chat with a little group.

There is âopen chat for current fileâ feature on SWISH.

What exactly do you mean by âcannedâ?

I wonder what kind of answer I expectedâŠ

Thanks to all for your help with SWISH. I will see this again tomorrow. I am out of internet this evening, from now. Bye bye !

Here is a snippet to publish the prover on your site.

/*  File:    minigui.pl
Author:  Carlo
Created: Sep 16 2020
Purpose: help on https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937
*/

:- module(minigui, []).

:- use_module(library(http/http_server)).
:- use_module(library(http/http_json)).
:- use_module(library(http/http_log)).

:- use_module(quine).

% when `make` just reload http://localhost:8082 to get changes
:- initialization (
Port=8082,
catch(http_stop_server(Port,[]),_,true),
http_server([port(Port)])
).

:- http_handler(root(.),
http_redirect(moved,location_by_id(home_page)),
[]).
:- http_handler(root(home),home_page,[]).

:- http_handler(root(eval_formula),eval_formula,[]).

home_page(_Request) :-
[ title('Quine prover')
],
[ div([
div([
label([
\formulae_predef,
'Choose a formula or input your one'
])
]),
textarea([
id=formula,
rows=4,cols=60,
title='enter your formula here, or select one predefined above'
],'?'),
div(button([id=eval_formula],[eval])),
pre([id=proof_show], 'proof will show here')
]),
\css,
\js
]).

formulae_predef --> html(select([id=formulae_predef],[
option('((P -> Q) -> P) -> P.'),
option('((A -> B) -> C) -> D.')
% add more, to illustrate accepted syntax
])).

eval_formula(Request) :-
open_string(Dict.formula,Stream),
(   call_with_time_limit(5,
with_output_to(string(Proof),
getFormula(Stream,Formula,Names,Tautology)))
->  with_output_to(string(Formula2), write_term(Formula:Tautology,[variables_names(Names)])),
),
close(Stream).

css --> html(style('

')).

js --> html(script("

const request = (url,json) => fetch(url,{
method: 'POST',
body: JSON.stringify(json)
}).then(r => r.json())

eval_formula.onclick = async (ev) => {
let f = formula.value.trim()
if (!f.endsWith('.')) f += '.'
try {
let result = await request('/eval_formula', {
formula:f
})
console.log(result)
proof_show.textContent = result.proof
} catch(e) {
}
}
formulae_predef.onchange = (ev) => {
formula.value = ev.target.value
}
}
")).

I had to change your file, since the recursive calls in quine/0 donât fit appropriately in this simple http scheme. So here it is - just wrapped in a module:

/*  File:    quine.pl
Created: Sep 16 2020
Purpose: help on https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937
*/

:- module(quine,
[quine/0
,getFormula/4
]).

/*
This prover is the work of Jan Burse. I changed only the symbols for operators, that's it.
See the web page : https://swi-prolog.discourse.group/t/implementing-quines-algorithm/2830
and also https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in?noredirect=1#comment112667699_63505466
the boole.pl original file is here: https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-boole-pl
*/

:- use_module(library(statistics)).

:- op(700, xfy, <=>).
:- op(600, xfy, =>).
:- op(500, xfy, v).
:- op(400, xfy, &).
:- op(300, fy, ~).

eval(A, A) :- var(A), !.
eval(A => B, R) :- !, eval(A, X), eval(B, Y), simp(X => Y, R).
eval(A <=> B, R) :- !, eval(A, X), eval(B, Y), simp(X <=> Y, R).
eval(A v B, R) :- !, eval(A, X), eval(B, Y), simp(X v Y, R).
eval(A & B, R) :- !, eval(A, X), eval(B, Y), simp(X & Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).

simp(A, A) :- var(A), !.
simp(A => _, 1) :- A == 0, !.
simp(A => B, X) :- B == 0, !, simp(~A, X).
simp(A => B, B) :- A == 1, !.
simp(_ => B, 1) :- B == 1, !.
simp(A <=> B, X) :- A == 0, !, simp(~B, X).
simp(A <=> B, X) :- B == 0, !, simp(~A, X).
simp(A <=> B, B) :- A == 1, !.
simp(A <=> B, A) :- B == 1, !.
simp(A v B, B) :- A == 0, !.
simp(A v B, A) :- B == 0, !.
simp(A v _, 1) :- A == 1, !.
simp(_ v B, 1) :- B == 1, !.
simp(A & _, 0) :- A == 0, !.
simp(_ & B, 0) :- B == 0, !.
simp(A & B, B) :- A == 1, !.
simp(A & B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).

judge(A, [B|R]) :-
eval(A, B),
term_variables(B, L),
judge(B, L, R).

% Boole prover
% First, write "boole" + Enter.
% Second, write your formula + Enter.

judge(_, [], R) :- !, R = [].
judge(A, [B|L], R) :-
copy_term(A-[B|L], C-[0|L]),
copy_term(A-[B|L], D-[1|L]),
judge(C & D, R).

boole :-
get_wff(_A,_L).

get_wff(A,L) :-
time(judge(A,L)),
last(L,R),
(
last(L,1) ->  write('to prove that the formula is a tautology, i.e. that its truth value is always '),
write(R),write(' .'),nl,nl,nl,
boole
;

last(L,0) -> write('to prove that the formula is not a tautology, i.e. that its truth value can be '),
write(R),write(' .'),nl,nl,nl,
boole
).

% Second prover, Quine prover more practical and more verbose:
% First, write "quine" + Enter.
% Second, write only your formula + Enter.

taut(A, T, N) :-
eval(A, B),
write_term(A, [variable_names(N)]),nl,
write_term(B, [variable_names(N)]),nl,
write('------------------------------'),nl,
term_variables(B, L), taut(B, L, T, N),nl.

/*
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0,taut(A, T, N), throw(T)), T, true),
B = 1, write(N),nl,nl,taut(A, S, N), T = S.
*/

taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 1,write(N),write(':'),nl,nl,taut(A, T, N),throw(T)), T, true),
B = 0,
write(N),write(':'),nl,nl,
taut(A, S, N), T = S.

quine:-
getFormula(current_input,_A,_N,_T).

getFormula(Stream, A, N, T) :-
(  time(taut(A, T, N))
-> /* here is the missing outer if-then-else */
(T == 1 ->
write('to prove that the formula is a tautology.')
;
write('to prove that the formula is an antilogy.')
)
;
write('to prove that the formula is neither a tautology nor an antilogy.')
).

You can try on your PC, just copy put the content in 2 files and launch swipl on minigui.pl.
Then browse http://localhost:8082.
Should work as well on your site, of course youâll need a running swipl there. But since youâre planning to go with SWISH (recommended but not so easy), youâre surely already aware of this.

Iâm just curious about PHP, because you cited it in the post title, and itâs one of mine daily âworking horsesâ. How is your site structured ?

3 Likes

@CapelliC
First, many thanks for these files, it was very kind of you to take time to write them to help me. I appreciate a lot.
I succeeded to load minigui.pl, but I do not understand why the result of proofs does not appear on the webpage. I have cp quine module into /var/www/html/ (local apache in my PC), and even in /var/www/html/home/ the result is the same: no proof inside the webpage âŠ I certainly missed something.

For this webpage of my webiste that with PHP, here are the files that are in /var/www/html/g4-prover/
First, g4action.php :

<!DOCTYPE html>
<html>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<body>
<?php
\$programmer = '<a href="https://www.vidal-rosset.net/?_Joseph-Vidal-Rosset_&lang=fr">Joseph Vidal-Rosset</a>';
\$back = '<a href="https://www.vidal-rosset.net/?G4-Prover&lang=en&var_mode=calcul">Back to <i>g4-prover</i></a>';
\$formula=\$_GET[formula];
\$system=fol;
\$sysopt=\$_GET[sysopt];
\$output=\$_GET[output];
file_put_contents(params4llprover,"g4.\n\n\$system(\$sysopt).\n\noutput(\$output).\n\n\$formula.\nquit.");
exec("swipl g4-prover.pl < params4llprover > linearesult");
\$r=file_get_contents(linearesult);
echo "<pre>
<h1>G4 Prover</h1>
<h3>Result of the test for sequent \$formula </h3>
<hr>
<br>
\$r
<h>
<hr>
<h3>\$back</h3>
<h3><i>Maintained by  \$programmer </i></h3>
</pre>";
?>
</body>
</html>

Second, index.php:

<html>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title> A Prover for Sequent Calculus G4</title>
<body>
<form method="get" action="g4action.php">
<ol>
<li> Please input a sequent in first order logic
<code><input size=50 name="formula"></code><br>
For example, <code>(p-> r)/\(q-> r) <-->  (p\/q)-> r</code>
or  <code>X#p(X)\/X#q(X) --> X#(p(X)\/q(X))</code>
<li> By default the prover is in intuitionistic logic, but you can choose another logic:
<select name="sysopt">
<option value="g4i" selected> G4i for intuitionistic logic
<option value="g4m"> G4m for minimal logic
<option value="g4c"> G4c for classical logic
</select>
</ul>
<li> Please select a output style:
<select name="output">
<option value="pretty" selected> Pretty form
<option value="tex"> LaTeX form
<option value="standard"> Indented form
<option value="term"> Internal form
</select>
<li> Now, press
<input type="submit" value="Prove">
or <input type="reset" value="Clear Input"><br>
</ol>
</form>
If you are looking for a sequent calculus prover for
first-order classical logic (LK),
<a href="https://www.vidal-rosset.net/?Sequent-Prover-seqprover">Sequent Prover (seqprover)</a>.
<hr>
<h2>Examples</h2>
All the following examples are valid in <i>classical logic</i>. When the prover fails in proving one of these formulas below, it means that this formula is not intuitionistically valid. Then, you can test its validity in G4c in the prover above and compare the ouput  with the result provided by <a href="https://www.vidal-rosset.net/?Sequent-Prover-seqprover">Naoyuki Tamura's prover</a>.
<ol>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5Ctop+%3C--%3E+p"><code>p/\top <-->  p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%5C%2Fbot+%3C--%3E+p"><code>p\/bot <-->  p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5Cbot+%3C--%3E+bot"><code>p/\bot <-->  bot</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%5C%2Ftop+%3C--%3E+top"><code>p\/top <-->  top</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5Cp+%3C--%3E+p"><code>p/\p <-->  p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%5C%2Fp+%3C--%3E+p"><code>p\/p <-->  p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5Cq+%3C--%3E+q%2F%5Cp"><code>p/\q <-->  q/\p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%5C%2Fq+%3C--%3E+q%5C%2Fp"><code>p\/q <-->  q\/p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5Cq+--%3E+p"><code>p/\q -->  p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5Cq+--%3E+q"><code>p/\q -->  q</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p+--%3E+p%5C%2Fq"><code>p -->  p\/q</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=q+--%3E+p%5C%2Fq"><code>q -->  p\/q</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5C%28q%2F%5Cr%29+%3C--%3E+%28p%2F%5Cq%29%2F%5Cr"><code>p/\(q/\r) <-->  (p/\q)/\r</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%5C%2F%28q%5C%2Fr%29+%3C--%3E+%28p%5C%2Fq%29%5C%2Fr"><code>p\/(q\/r) <-->  (p\/q)\/r</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5C%28q%5C%2Fr%29+%3C--%3E+%28p%2F%5Cq%29%5C%2F%28p%2F%5Cr%29"><code>p/\(q\/r) <-->  (p/\q)\/(p/\r)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%5C%2F%28q%2F%5Cr%29+%3C--%3E+%28p%5C%2Fq%29%2F%5C%28p%5C%2Fr%29"><code>p\/(q/\r) <-->  (p\/q)/\(p\/r)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5C%28q%5C%2Fr%29+--%3E+%28p%5C%2Fq%29%2F%5C%28p%5C%2Fr%29"><code>p/\(q\/r) -->  (p\/q)/\(p\/r)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%28p%2F%5Cq%29%5C%2F%28p%2F%5Cr%29+--%3E+p%5C%2F%28q%2F%5Cr%29"><code>(p/\q)\/(p/\r) -->  p\/(q/\r)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%7E+%7E+p+%3C--%3E+p"><code>~ ~ p <-->  p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5C+%7Ep+%3C--%3E+bot"><code>p/\ ~p <-->  bot</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%5C%2F+%7Ep+%3C--%3E+top"><code>p\/ ~p <-->  top</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%7E%28p%2F%5Cq%29+%3C--%3E+%7Ep%5C%2F+%7Eq"><code>~(p/\q) <-->  ~p\/ ~q</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%7E%28p%5C%2Fq%29+%3C--%3E+%7Ep%2F%5C+%7Eq"><code>~(p\/q) <-->  ~p/\ ~q</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p-%3Eq+%3C--%3E+%7Ep%5C%2Fq"><code>p-> q <-->  ~p\/q</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%7Ep+%3C--%3E+p-%3Ebot"><code>~p <-->  p-> bot</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p-%3Eq+%3C--%3E+%7Eq-%3E+%7Ep"><code>p-> q <-->  ~q->  ~p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p-%3Eq-%3Er+%3C--%3E+q-%3Ep-%3Er"><code>p-> q-> r <-->  q-> p-> r</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p-%3Eq-%3Er+%3C--%3E+%28p%2F%5Cq%29-%3Er"><code>p-> q-> r <-->  (p/\q)-> r</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%28p-%3Eq%29%2F%5C%28p-%3Er%29+%3C--%3E+p-%3Eq%2F%5Cr"><code>(p-> q)/\(p-> r) <-->  p-> q/\r</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%28p-%3Er%29%2F%5C%28q-%3Er%29+%3C--%3E+%28p%5C%2Fq%29-%3Er"><code>(p-> r)/\(q-> r) <-->  (p\/q)-> r</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p-%3Eq%2C+q-%3Er+--%3E+p-%3Er"><code>p-> q, q-> r -->  p-> r</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p--%3E%28q-%3Ep%29"><code> p --> (q-> p)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%28p-%3E%28q-%3Er%29%29--%3E%28%28p-%3Eq%29-%3E%28p-%3Er%29%29"><code>(p-> (q-> r))--> (p-> q)-> (p-> r)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%28p-%3E+%7Eq%29--%3E%28%28p-%3Eq%29-%3E+%7Ep%29"><code>p-> ~q --> (p-> q)->  ~p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%28%7Ep-%3E+%7Eq%29--%3E%28%28%7Ep-%3Eq%29-%3Ep%29"><code> ~p->  ~q --> (~p-> q)-> p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%2F%5C%28p-%3Eq%29%2F%5C%28p%2F%5Cq-%3Es%29--%3Es"><code>p/\(p-> q)/\(p/\q-> s)--> s</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=top--%3Ep%5C%2F%28p-%3Eq%29"><code>top --> p\/(p-> q)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=((p->q)->p)-->p"><code>((p-> q)-> p)--> p</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=top-->X@p(X)->p(a)/\p(b)"><code>top-->X@p(X)-> p(a)/\p(b)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=p%28a%29%5C%2Fp%28b%29+ --%3E+X%23p%28X%29"><code>p(a)\/p(b) -->  X#p(X)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=X@X@p%28X%29+%3C--%3E+X@p%28X%29"><code>X@X@p(X) <-->  X@p(X)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=X%23X%23p%28X%29+%3C--%3E+X%23p%28X%29"><code>X#X#p(X) <-->  X#p(X)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=X@%28p%28X%29%2F%5Cq%28X%29%29+%3C--%3E+X@p%28X%29+%2F%5C+X@q%28X%29"><code>X@(p(X)/\q(X)) <-->  X@p(X) /\ X@q(X)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=X%23%28p%28X%29%5C%2Fq%28X%29%29+%3C--%3E+X%23p%28X%29+%5C%2F+X%23q%28X%29"><code>X#(p(X)\/q(X)) <-->  X#p(X) \/ X#q(X)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%7EX@p%28X%29+%3C--%3E+X%23%28%7Ep%28X%29%29"><code>~X@p(X) <-->  X#(~p(X))</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%7EX%23p%28X%29+%3C--%3E+X@%28%7Ep%28X%29%29"><code>~X#p(X) <-->  X@(~p(X))</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%7EX@%28p%28X%29-%3Eq%28X%29%29+%3C--%3E+X%23%28p%28X%29%2F%5C+%7Eq%28X%29%29"><code>~X@(p(X)-> q(X)) <-->  X#(p(X)/\ ~q(X))</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=%7EX%23%28p%28X%29%2F%5Cq%28X%29%29+%3C--%3E+X@%28p%28X%29-%3E+%7Eq%28X%29%29"><code>~X#(p(X)/\q(X)) <-->  X@(p(X)->  ~q(X))</code></a> <span style="color:red">SLOW!</span>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=X@p%28X%29+--%3E+X%23p%28X%29"><code>X@p(X) -->  X#p(X)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=top--%3E+Y%23X@%28p%28X%29-%3Ep%28Y%29%29"><code>top --> Y#X@(p(X)-&gt;p(Y))</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=X%23Y@p%28X%2CY%29+--%3E+Y@X%23p%28X%2CY%29"><code>X#Y@p(X,Y) -->  Y@X#p(X,Y)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=top--%3E+%28p%28a%29%2F%5Cp%28b%29-%3Eq%29-%3EX%23%28p%28X%29-%3Eq%29"><code>(p(a)/\p(b)-> q)-> X#(p(X)-> q)</code></a>
<li><a href="g4action.php?sysopt=g4i&output=pretty&formula=n(0), X@(n(X)-> n(s(X))) -->  n(s(s(0)))"><code>n(0), X@(n(X)-> n(s(X))) -->  n(s(s(0)))</code></a>
</ol>
<hr>
</body>
</html>

The file g4-prover.pl can be dowloaded from the g4-prover webpage.

The other files (linearesult and params4llprover) are written and updated by input via php (I have just checked it locally).

I have tried to follow this example for quine.pl but I get a indefinite loop : the file quineresult becomes bigger and bigger, I do not understand why.

Hoping to help in turn.
Best wishes.

Letâs start simpler, on your PC, after you have put in any folder (not necessarily the Apache server root) the 2 files (minigui.p,quine.pl), should be enough to start swipl and consult minigui.
Then localhost:8082 will show the page as you attached above, try to open the JS developer tools (Ctrl+i in Chrome, Ctrl+Shift+i in Firefox), input a formula, and press the proof button. In console there should be some feedback, otherwise weâll need to put some console.log in the minigui.pl JS script to track what happens.
Sorry for the late reply, this morning the discourse site was not fully operational, so I didnât saw your reply, and right now I must move to the office.
Will resume supporting this evening, if you are still interested.

1 Like

@CapelliC

Your reply is not late at all ! Do not be sorry. Every one helps when he can. I am going to try to follow your instructions in order to know more. Thanks again.

Here is the error message :

code: 500
â
message: "Stream <stream>(0x555c31983800):1:2 Syntax error: Unexpected end of file"