Jean-Luc-Picard-2021

Example that sends tree tool into nirwana

3

I tried this here: > ∀x(m(e,x)=x)∧∀x(m(i(x),x)=e)∧∀x∀y∀z(m(m(x,y),z)=m(x,m(y,z)))→∀x(m(x,e)=x) https://www.umsu.de/trees/#~6x(m(e,x)=x)~1~6x(m(i(x),x)=e)~1~6x~6y~6z(m(m(x,y),z)=m(x,m(y,z)))~5~6x(m(x,e)=x) But it gets very quickly into a state where stop buttion doesn't work anymore. Bug or feature?

Hi, I am quite amazed by your tool, since it not only searches a proof, it also tries to find a counter model at the same time. I am currently...

Does the tree tool search shortest proofs?

2

What is the search strategy for proofs? Some iterative deepening. Here is a funny example, where I find a shorter regular proof for FOL with equality, its a validation proof,...

Is there something like `format_time/3` in GNU Prolog? I found for example this in SWI-Prolog which uses a certain convention concerning the format specifiers: > **format_time(+Out, +Format, +StampOrDateTime)** https://www.swi-prolog.org/pldoc/man?predicate=format_time/3 I...

Ubuntu defaults so that GNU compile result is speedy

1

Was compiling GNU Prolog 1.6.0 on WSL2 / Ubuntu, but the result is only half as fast as the GNU Prolog 1.4.5 distribution. How can I compile it to get...

ensure_loaded/1 wants suddently predicate indicator

1

In Version 1.4.5 I get:  In Version 1.6.0 I get:  I don't see this behaviour documented: When such a directive is encountered it is simply ignored. http://www.gprolog.org/manual/gprolog.html#sec59

Some testing: ``` /* GNU Prolog 1.5.0 */ ?- X = f(A,X), numbervars(X, 0, _), write_canonical(A), nl. _24 cannot display cyclic term for X /* SWI-Prolog 9.1.16 */ ?- X...

real_file_name does not follow symlinks on Windows

1

Is there a way to retrieve a real file name in GNU Prolog, that results from following symlinks? Take this scenario of a file symlink on Windows: ``` >dir foo...

Try this: ``` test(X) :- append(Y, X, [1,2,3|Y]). ``` I get that GNU Prolog cannot run it indefinitely: ``` ?- test(X). X = [1,2,3] ? ; X = [2,3,1] ?...

I had this source code: ``` deadfish_(X, X) --> [o]. % Output always at the end deadfish_(X0, X) --> { ops(Op, X0, X1) }, [Op], deadfish_(X1, X). ``` But by...