These two files given by Carlo are a Quine prover that in my local apache2 work very well now. First minigui.pl:
/* 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:
/* 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:
((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:
- How to do to make this prover working on a website?
- On SWISH with two files?
Thanks for your help !
