@CapelliC @anon95304481 @jan
These two files given by Carlo are a Quine prover that in my local apache2 work very well now. First minigui.pl:
```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, [op(700, xfy, <=>),
op(600, xfy, =>),
op(500, xfy, v),
op(400, xfy, &),
op(300, fy, ~)
]).
:- use_module(library(http/http_server)).
:- use_module(library(http/http_json)).
:- use_module(library(http/http_log)).
:- use_module(library(statistics)).
:- use_module(quineweb).
% 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) v (B => A).'),
option('(~ A => A) <=> ~ ~ A.'),
option('(~ A & A) => B'),
option('(A => ~ A) <=> ~ A')
% 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,[variable_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
}
}
")).
```
and now quineweb.pl:
```prolog
/* File: quineweb.pl
Created: Sep 16 2020
Purpose: help on https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937
*/
:- module(quineweb,
[quine/0,
getFormula/4,
op(700, xfy, <=>),
op(600, xfy, =>),
op(500, xfy, v),
op(400, xfy, &),
op(300, fy, ~)
]).
/*
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)).
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.')
).
```
Example of output:
```prolog
((A=>B)=>A)=>A
((A=>B)=>A)=>A
------------------------------
[A=1,B=_6360]:
((1=>B)=>1)=>1
1
------------------------------
[A=0,B=_6360]:
((0=>B)=>0)=>0
1
------------------------------
to prove that the formula is a tautology.
```
A detail: the mention of the result of time/1 is not given on the html file, but only in the background, in my Prolog session in emacs. I do not know how to fix it.
Two questions:
1. How to do to make this prover working on a website?
2. On SWISH with two files?
Thanks for your help !
---
Use `:- include(file).` The `file` is the plain file name (without `.pl`) of a saved _program_. Files can include each other (even cyclic) and notebook program cells can include files. As yet, there is no way to include a program cell from another notebook.
The main drawback is that if you modify the included program you have the save it before the changes get visible in the programs and notebooks that include the file.
Note that saved programs can also be reused through the Pengines API.
---
Thanks. I realize that my 2 files question was stupid because the function of minigui.pl is to load the prover in local with apache2. Sorry.
@CapelliC
I would be glad to know how I can use this couple of files in my website , i.e. into a quine directory with an index.php …
---
SWISH is certainly very nice, but with the program below that provides results of Quine tests, I do not see how it is possible to use SWISH in the same way than in a browser via the two files given by Carlo (even I do not know still how to adapt them to publish the prover online).
```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)) ->
(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
).
```
I do not succeed to get in SWISH the same type of output that I get in my emacs after having written “quine.” and enter my formula…
---
Joseph, do you have access to your server command line ?
If yes, copy the 2 files (with FTP?) on a directory in your server, not necessarily the Apache root folder (usually on Ubuntu /var/www/html), and start the swipl server with
```prolog
$ swipl minigui.pl
```
as you do on your PC. If this works, you should be able to access with your public address, i.e.
[https://www.vidal-rosset.net:8082](https://www.vidal-rosset.net:8082)
Sorry I don’t have a public http server available to test myself.
Yesterday evening I did a fair amount of work on the PHP interface, not fully functional yet,
but I progressed… will let you know, maybe tomorrow…
Forgive me for the stupid bug about operators (to be true, rather unexpected, given that the quine module calls read, and there the operators should be already declared… I will test), sometime the most obvious things get hidden by other details.
Ciao, Carlo
---
Thanks Carlo, you are really very kind.
I tried:
root@sd-118693:/var/www/html# swipl minigui.pl
% Started server at [http://localhost:8082/](http://localhost:8082/)
Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.3)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.
For online help and background, visit [https://www.swi-prolog.org](https://www.swi-prolog.org)
For built-in help, use ?- help(Topic). or ?- apropos(Word).
but at [https://www.vidal-rosset.net:8082](https://www.vidal-rosset.net:8082) the server does not respond… ☹
I will see that tomorrow.
Best wishes, and again, thanks !
---
> [@joseph-vidal-rosset](#):
>
> the server does not respond…
Some days ago there has been a discussion about https, will try to understand better,
because serving html directly from swipl seems the better choice to me.
But meantime, I’ve worked out an approximately equivalent interface in PHP:
```prolog
['pipe','r'],
1 => ['pipe','w'],
//2 => null
];
$proc = proc_open("swipl -g quine -g halt $quine", $descp, $pipes);
if (is_resource($proc)) {
fwrite($pipes[0], $formula);
fclose($pipes[0]);
$Proof = stream_get_contents($pipes[1]);
fclose($pipes[1]);
$return_value = proc_close($proc);
header('Content-type: application/json');
echo json_encode(['proof'=>$Proof,'formula'=>'TBD']);
}
exit;
}
?>
Quine prover
proof will show here
**Author:**  [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\
**Post date:** [September 19, 2020, 7:28am UTC](https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937/66 "2020-09-19T07:28:16Z")
Many thanks Carlo. I am going to test this file immediately.
---
@CapelliC
Good news Carlo, it works perfectly !!! Many many thanks, I hope it will be useful also for my students.
[https://www.vidal-rosset.net/quine/](https://www.vidal-rosset.net/quine/)
---
@anon95304481
> For proof stuff, this here seems to also work inside [SWISH](https://swish.swi-prolog.org/).
Reading your Hilbert.pl, it seems to me that it is also because I do not know how to write output in Prolog that this Quine prover as well as truth\_table\_maker.pl does not work well in SWISH. The best that I can print in SWISH with Quine prover is this:
```prolog
N = A=>A,
T = []
```
☹
---
> [@joseph-vidal-rosset](#):
>
> Good news Carlo, it works perfectly !!!
I gave it a test run. Nice work everyone.
* * *
Still going to stress the point that it should be easy to understand and use.
Many programmers are familiar with [Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus) but trying to find something that makes it easy to show how to simplify and evaluate Lambda Calculus expressions is not easy. I specifically chose the words `evaluate` and `simplify` in that sentence because I suspect they are ringing in your head at this point.
While the demonstration on the [page](https://www.vidal-rosset.net/quine/) you have published makes it much easier to see the evaluation and simplification of a Quinie prover, if I were to visit the page I would have no idea what a `Quine Prover` is without doing some research, and thus probably walk away from it.
Here is a site that I have been referencing for years that does what I note but for Lambda Calculus:
Explanation page: [Lambda calculus reduction workbench](http://www.itu.dk/people/sestoft/lamreduce/)
Evaluator page: [Workbench](http://www.itu.dk/people/sestoft/lamreduce/lamframes.html)
In other words is someone were to visit the [Workbench](http://www.itu.dk/people/sestoft/lamreduce/lamframes.html) first they might be confused, but if they visit the [explanation page](http://www.itu.dk/people/sestoft/lamreduce/) first then they might find it more interesting. 🙂
---
@EricGT
Thanks for these webpage and for your visit! The Quine Prover webpage is at the moment a work in progress. I plan to write an explanation of the rules, of course.
Best wishes,
Jo.
---
@anon95304481 @CapelliC
> **[Quine Prover for Classical Propositional Logic](https://www.vidal-rosset.net/quine_prover_for_classical_propositional_logic.html)**
That is only a first draft, and the presentation of the prover must be still improved.
@anon95304481 I wonder about the rules and the priorities that could be defined for _fell swoops_.
---
> [@anon95304481](#):
>
> My program didn’t do that, it would use sys\_print\_map. Maybe you could fix it as well through some use with variable names in write term. Or it would build the filtered list on the fly, avoiding any variable name display issue.
Yes, I agree that it would be far better to avoid the print of variables Prolog. I have tried to find a function to do it, but without success. Here is quineweb.pl that is the program behind this web page:
```prolog
/* File: quineweb.pl
Created: Sep 16 2020
Purpose: help on https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937
*/
:- module(quineweb,
[quine/0,
getFormula/4,
op(700, xfy, <=>),
op(600, xfy, =>),
op(500, xfy, v),
op(400, xfy, &),
op(300, fy, ~)
]).
/*
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)).
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.')
).
```
The relevant lines are :
```prolog
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.
```
One needs a filter on N to prevent variables printing.
---
> [@anon95304481](#):
>
> Do you have your code on GitHub, so that can make tickets and dont need to post full code here everytime? Do you use some IDE? Most IDEs have GitHub plug-ins.
Yes, I have a github page, but I do not use it rationally. I will think about it. I’m using emacs, and emacs only.
[Previous page](https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937.md?page=2)
[Next page](https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937.md?page=4)