SWI-Prolog - PHP - Html


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

https://swish.swi-prolog.org/p/truth_table_maker.swinb I hope it is good now. Thanks !

@j4n_bur53 @jan

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 {
      let result = await request('/eval_formula', {
      if (result.proof)
        proof_show.textContent = result.proof
        proof_show.innerHTML = 'there was a problem:<b>'+JSON.stringify(result)+'<b>'
    } catch(e) {

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):






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.

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 :slight_smile:

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.


@jan Thanks for your answer. I understand that I have a lot to learn. That’s it. :slight_smile:

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,

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) :-
    read_term(A, [variable_names(_N)]),
	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,

    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,

% 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,
    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,
  taut(A, S, N), T = S.


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.




% 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.


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.


Really nice !