https://swish.swi-prolog.org/p/truth_table_maker.pl can certainly be still improved.

What are exactly the differences between a Prolog notebook and a Prolog program on SWISH ?

Notebooks are really good for telling a story; you can mix html elements with code and queries on the code to explain something.

Thanks for this point!

Is fixed and SWISH is updated.

Seems like you have hit the eval button when the page has been (re)loaded, without input any formula in the text box (that is, the editable area where you see the `?`

), or selected anything from the combo box (where BTW you should add some formulae as examples of the accepted syntax).

Try to replace the javascript function you find near line 86 of minigui.pl with

```
eval_formula.onclick = async (ev) => {
let f = formula.value.trim()
if (!f.endsWith('.')) f += '.'
try {
console.log('formula',f)
let result = await request('/eval_formula', {
formula:f
})
console.log('result',result)
if (result.proof)
proof_show.textContent = result.proof
else
proof_show.innerHTML = 'there was a problem:<b>'+JSON.stringify(result)+'<b>'
} catch(e) {
alert(e.message)
}
}
```

Anyway, from a quick inspection of the PHP file you have posted, I think this interface will not be much useful.

Most probably you donāt have access to (or donāt use) the command line of your server, and this is required to start SWI-Prolog HTTP server process.

The whole point of my script was to show a **minimal** setup, that doesnāt fit well with your server setupā¦ sorry.

Maybe you could take inspiration from the interface Iāve shown to adapt the PHP file. Will try now to provide some hints for that.

Hi, I wanted to tell you that it works finally (before your last suggestion that I will try):

```
A->B
A->B
------------------------------
[A=1,B=_6260]:
1->B
1->B
------------------------------
[A=1,B=1]:
1->1
1->1
------------------------------
[A=1,B=0]:
1->0
1->0
------------------------------
to prove that the formula is neither a tautology nor an antilogy.
```

But there is a problem with operators: as you can see here ā -> ā and not '=> ā and it does not work for disjunction nor for conjunction &.

Effectively, I didnāt put any effort in searching for valid formulae, just correct (and add) them in minigui.pl. Itās pretty readable, I thinkā¦ They are here

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

There is also a bug you should fix, look for this line

```
-> with_output_to(string(Formula2), write_term(Formula:Tautology,[variables_names(Names)])),
```

and replace `variables_names`

with `variable_names`

.

If you use XPCE editor, just recompile (Ctrl+b) and reload the page. Otherwise, enter

```
?- make.
```

in swipl interface. No need to shutdown and restartā¦

Many thanks for your so kind help. I will look this again tomorrow now. We stay in touch. I will keep you informed !

You are not using the *table renderer*, but simply displaying answers in a table row. The renderers handle a single answer. The table one is discussed in https://swish.swi-prolog.org/example/render_table.swinb. It is pretty basic though.

@j4n_bur53

Hi Jan . It seems to me that SWISH and publication of Prolog provers online have different goals. The latter has to be user friendly as much as possible, that is to say, the user write only his formal to test it, type Enter, thatās it. It seems that SWISH does not allow (at least not directly) such a function: a minima the user has to write prolog_function(formula), that is a predicate/1, it means that he has to be aware of Prolog queries. SWISH is a very nice tool to share and test programs in the Prolog community, thatās different.

You found one way. Embedded HTML is another solution, see https://swish.swi-prolog.org/example/htmlcell.swinb

No. Well, probably yes as you can access the interface. See https://swish.swi-prolog.org/example/jquery.swinb

Interaction is not the strong point of SWISH. Normally, interaction is one-shot where a query creates a Pengine on the server that dies afterwards. If you want to make it live longer you have (I think) two options. One is to use read/1 or some other read predicate to read the next action and the other is to use an HTML cell and create a server Pengine by hand to make it do whatever you want. In theory you can do anything you can do using HTML and JavaScript in a browser and server side Pengines within the limitations of the sandbox. That is quite a lot

Nope. You can write full web applications in SWISH. See e.g., https://swish.swi-prolog.org/example/chat80.swinb. There is still a hamburger menu to go back to normal SWISH mode, but as you can use JavaScript you can easily hide that too. This example uses the default SWISH answer renderer, but you can change that as well.

I consider this one of the big benefits of SWISH. You can play online in a more or less conventional Prolog toplevel. You can add output rendering to get nice answers, next notebooks to make it appeal to a wider audience and finally a full fetched web application where you can no longer see it is Prolog/SWISH based. You can do all this stuff online without installing anything and you can even collaborate while building it.

@CapelliC

I do not understand why the file below that I call quineweb.pl (your quine.pl) do *not* use the operators (i.e. the propositional connectives ~ , & , v , => that are defined in this file :

```
/* File: quineweb.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.')
).
```

Here is what I mean:

```
?- quine.
|: A => A.
ERROR: Stream user_input:11:5 Syntax error: Operator expected
?- quine.
|: A -> A.
A->A
A->A
------------------------------
[A=1]:
1->1
1->1
------------------------------
[A=0]:
0->0
0->0
------------------------------
% 50 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 495958 Lips)
to prove that the formula is neither a tautology nor an antilogy.
true.
?-
```

Note also that the comment is not the good one. I have to leave my PC. See you later.

As I claimed, it is pretty basic. Possibly it should be extended a bit. There will always be limits using this approach though. The intend of renderers such as the table renderer is to give you something quick and dirty if you have a Prolog data structure that is ātable likeā, much like portray/1 does for plain Prolog.

You can get cute tables using the HTML output facilities. See https://swish.swi-prolog.org/example/html_output.swinb

Thanks Jan, thanks again and again.

Nope. It is still just rendering Prolog answers. Using the SWISH HTML writing gets the nicest looking result. There is an example generating a Bootstrap table in the docs I linked before.