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 !
```prolog
/*
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) :-
read_term(A, [variable_names(_N)]),
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) :-
read_term(A, [variable_names(N)]),
(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
).
```
---
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](https://swi-prolog.discourse.group/t/yet-another-web-applications-tutorial/566) very useful!
Cheers/JC
---
SWISH is probably not the solution:
```prolog
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.
---
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](https://en.wikipedia.org/wiki/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](https://www.vidal-rosset.net/g4-prover/) . 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.
---
> [@joseph-vidal-rosset](#):
>
> [SWISH](https://swish.swi-prolog.org/) is probably not the solution:
I’ll add that. read/1 works. I think read\_term/2 is also safe regardless of the options.
---
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
```prolog
read_line_to_string(user_input, S),
term_string(Term, S, [variable_names(Names)]).
```
See [https://swish.swi-prolog.org/p/hiduyzWI.swinb](https://swish.swi-prolog.org/p/hiduyzWI.swinb)
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](https://www.vidal-rosset.net) or if it is still better to save theses prolog provers on a SWISH instance somewhere else.
@anon95304481 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](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](http://lpsdemo.interprolog.com/p/unsat.pl) But before going on I prefer to ask @anon95304481 his agreement.
---
> [@anon95304481](#):
>
> Didactically I would recommend using a version with Prolog atoms and not with Prolog logical variables. The solution with Prolog logical variables is a little “hacky”.
Hacky but more efficient, as you know it. 😉
> [@anon95304481](#):
>
> If you want precedent work of Quine algorithm, you can check [fCube](http://www2.disco.unimib.it/fiorino/fcube.html).
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.
> [@anon95304481](#):
>
> I use the same approach in my code, when I adopt foreign code.
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.
---
> [@anon95304481](#):
>
> How about a new [sys\_print\_map](https://github.com/SWI-Prolog/swipl-devel/issues/659) flag. And its integration with [SWISH](https://swish.swi-prolog.org/) as well. The [read\_term/2](https://www.swi-prolog.org/pldoc/doc_for?object=read_term/2) is only there for those algorithms, like my Quine or others that are to come, that use Prolog logical variables. It wouldn’t really be needed for Prolog atom solutions.
I got it. I will therefore publish the program that I adapted from Isabelle Newbie’s .
> [@anon95304481](#):
>
> You could then present “logic teaching” as a series of canned “?-” queries. Further one might consider to provide a proof tree filter, similar like you have table filters, etc… So an output might return a proof object, and this proof object is rendered inside [SWISH](https://swish.swi-prolog.org/).
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.
---
> [@joseph-vidal-rosset](#):
>
> I am searching something where I can chat with a little group.
There is “open chat for current file” feature on SWISH.
---
Here is a snippet to publish the prover on your site.
```prolog
/* 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) :-
reply_html_page(
[ 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) :-
http_read_json_dict(Request,Dict),
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)])),
reply_json_dict(_{proof:Proof,formula:Formula2})
; reply_json_dict(_{proof:failed})
),
close(Stream).
css --> html(style('
')).
js --> html(script("
window.onload = () => {
const request = (url,json) => fetch(url,{
method: 'POST',
headers: { 'Content-Type': 'application/json' },
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) {
alert(e.message)
}
}
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:
```prolog
/* 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) :-
read_term(A, [variable_names(_N)]),
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) :-
read_term(Stream, A, [variable_names(N)]),
( 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](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 ?
---
@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](https://www.vidal-rosset.net/g4-prover/) of my webiste that with PHP, here are the files that are in /var/www/html/g4-prover/
First, g4action.php :
```prolog
Joseph Vidal-Rosset';
$back = 'Back to g4-prover';
$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 "
G4 Prover
Result of the test for sequent $formula
$r
$back
Maintained by $programmer
";
?>
```
Second, index.php:
```prolog
A Prover for Sequent Calculus G4
If you are looking for a sequent calculus prover for
first-order classical logic (LK),
please check
Sequent Prover (seqprover).
Examples
All the following examples are valid in classical logic. 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 Naoyuki Tamura's prover.
```
The file g4-prover.pl can be dowloaded from the [g4-prover webpage](https://www.vidal-rosset.net/g4-prover/).
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.
---
> [@joseph-vidal-rosset](#):
>
> no proof inside the webpage
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.
---
> [@CapelliC](#):
>
> Sorry for the late reply
@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 :
```prolog
code: 500
message: "Stream (0x555c31983800):1:2 Syntax error: Unexpected end of file"
```
[Next page](https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937.md?page=2)