SWI-Prolog - PHP - Html

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.

1 Like

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

/*
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

$ 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

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/
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
For built-in help, use ?- help(Topic). or ?- apropos(Word).
but at https://www.vidal-rosset.net:8082 the server does not respond… :frowning:

I will see that tomorrow.
Best wishes, and again, thanks !

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:

<?php

/*  File:    minigui/index.php
    Author:  Carlo
    Created: Sep 18 2020
    Purpose: help on https://swi-prolog.discourse.group/t/swi-prolog-php-html/2937
*/

/*  With swipl http dispatch support, we were able to handle
    http requests right inside the script, in php we must handle
    more low level details...
    Here is the (roughly) equivalent of predicate eval_formula/1.
    It's all about low level interface details, that we can ignore
    when running on swipl http server library...
*/

if ($f_encoded = ($_POST['formula'] ?? null)) {

  $formula = urldecode($f_encoded);
  
  // swipl will need the full path, so
  // assume quine.pl is in the same folder as this php script
  $quine = __DIR__ . '/quine.pl';
  $descp = [
    0 => ['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;
}

?>
<!DOCTYPE html>
<html>
  <head>
    <meta charset="utf-8">
    <title>Quine prover</title>
  </head>
  <div>
    <div>
      <label>
        <?=formulae_predef()?>
        Choose a formula or input your one
      </label>
    </div>
    <textarea id=formula rows=4 cols=60 title='enter your formula here, or select one predefined above'>
A
    </textarea>
    <div>
      <button id=eval_formula>eval</button>
      <pre id=proof_show>proof will show here</pre>
    </div>
  </div>
  <?=css()?>
  <?=js()?>
</html>
<?php

function formulae_predef() {
  ob_start();?>
  <select id=formulae_predef>
    <option>((P => Q) => P) -> P .</option>
    <option>((A <=> B) v C) & D .</option>
    <!-- add more, to illustrate accepted syntax -->
  </select>
  <?php return ob_get_clean();
}

function css() {
  ob_start();?>
<style>
</style>
  <?php return ob_get_clean();  
}

function js() {
  ob_start();?>
  <script>
window.onload = () => {

  const request = (url,formula) => fetch(url,{
    method: 'POST',
    headers: { 'Content-Type': 'application/x-www-form-urlencoded;charset=UTF-8' },
    body: 'formula='+encodeURIComponent(formula)
  }).then(r => r.json())

  eval_formula.onclick = async (ev) => {
    let f = formula.value.trim()
    if (!f.endsWith('.')) f += '.'
    try {
      let result = await request("<?=$_SERVER['REQUEST_URI']?>", f)
      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)
    }
  }
  formulae_predef.onchange = (ev) => {
    formula.value = ev.target.value
  }
}
  </script><?php
  return ob_get_clean();
}

This index.php should go into the Apache folder, maybe the path could be /var/www/html/minigui, together with quine.pl (or quineweb.pl, but then remember to correct the file name at line 23)

Then should be available at
https://www.vidal-rosset.net/minigui

1 Like

Many thanks Carlo. I am going to test this file immediately.

@j4n_bur53
That is as pretty as impressive !

@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/

2 Likes

@j4n_bur53

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:

N = A=>A,
T = []

:frowning:

@j4n_bur53

I prefer the first version with tables in SWISH . But I guess that you want to test several options.

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 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 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
Evaluator page: Workbench

In other words is someone were to visit the Workbench first they might be confused, but if they visit the explanation page first then they might find it more interesting. :slightly_smiling_face:

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

1 Like

@j4n_bur53 @CapelliC

That is only a first draft, and the presentation of the prover must be still improved.

@j4n_bur53 I wonder about the rules and the priorities that could be defined for fell swoops.

1 Like

Nice!

Really like the introduction page. :+1:

How many do you think understood the empty square?

@j4n_bur53

I just corrected the link, you are right . I will fix the output of the program in next days.

I do not know.

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:

/*  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 :

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.

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.

@j4n_bur53
But now the print of “full sweep” is not complete:

?- quine.
|: A => (B => A).
A=>B=>A
A=>B=>A
------------------------------
A = 1:

1=>B=>1
1
------------------------------
% 42 inferences, 0.000 CPU in 0.000 seconds (94% CPU, 225019 Lips)
to prove that the formula is neither a tautology nor an antilogy.
true.

:frowning:

I have corrected my error. It works smoothly now. Thanks !