From Newsgroup: sci.logic

Hi,

Ok, I see, its not really a Prolog.
For example I get the below. Why
does it have ISO compliance tests?

?- T = f(Y,Z,S), f(X,Y,Z) = T.
(no answers)
https://eyereasoner.github.io/eyeprolog/playground

Whoever payed for this nonsense, had
his money lavishly thrown out of a
window. They could use the australian

gas to directly burn some dollar notes.

LoL

Bye

Mild Shock schrieb:

Hi,

Its interesting that we already have
like for 50 years the Curry Howard
isomorphims, as proof justifications terms,

Still it seems extremly hard to generate
proof certificates for Prolog, isn't it?
How it started:

Ai x Big Gas. What could go wrong? https://www.youtube.com/watch?v=kON2ZI2BNj8

How its going:

eq(Z,Z).
why eq(f(X,a),f(b,Y))
eq(f(b, a), f(b, a)).
why(
-a eq(f(b, a), f(b, a)),
-a proof(
-a-a-a goal(eq(f(b, a), f(b, a))),
-a-a-a by(fact("<input>", clause(1))),
-a-a-a bindings([binding("Z", f(b, a))])
-a )
).
https://eyereasoner.github.io/eyeprolog/playground

Truely some bullshit authorized by Sarah Connor.
So far there is no danger of an upcoming
Skynet that will gain self-awareness.

Bye

Mild Shock schrieb:

Hi,

Now the SWI community has create a new circus
example, probably AI generated by a prompt
enginerring, add a silly greeting line:

A: Thank you so much for sharing information
-a-a-a about the LogicBiz V.2.0 project!
B: Thank you so much for your kind words
-a-a-a and encouragement!
A: Thank you so much for your honest and
-a-a-a heartfelt reply!
B: Thank you so much for your heartwarming
-a-a-a and supportive reply!
A: Thank you for your openness!
B: Thank you for your valuable feedback!
A: Thank you for sharing such a detailed
-a-a-a and impressive technical breakdown!
B: Thank you for the detailed breakdown!
A: Thank you for the fascinating perspective!
https://swi-prolog.discourse.group/t/the-unrusting-blade-an-offline-first-logicbiz-v-2-0-powered-by-swi-prolog-sqlcipher-reply-01/9752


The pinacle of their "logic programming":

"Barcode Scanners & EDC inputs: Barcode scanners
inherently act as Human Interface Devices (HID) rCo
meaning they just inject keyboard strokes into
the active field. Since my input terminal is
already standard web HTML, a physical USB/Bluetooth
scanner works instantly out-of-the-box without
needing complex C/C++ bindings or custom drivers
in Prolog. The same applies to manually
entering EDC trace codes."
https://swi-prolog.discourse.group/t/the-unrusting-blade-an-offline-first-logicbiz-v-2-0-powered-by-swi-prolog-sqlcipher-reply-01/9752


Thank you for your unhinged nonsense!

Bye

P.S.: Isn't following georgi gerganov or
andrej karpathy more exciting. What if you
want to integrate a chatbot into your web

storefront, which is not a point of sale,
but a pizza ordering web site? Do it with
uber eats out of the box. Are we already lost?

Or can we rise without burning?

Mild Shock schrieb:

Hi,

The SWI-Prolog community is a circus.
I mean there are not only clowns like
Boris the Loris and Nazi Retard Julio,

there are also clowns like completely
mentally deranged Philosophy Professors,
such as Joseph Vidal Rosset.

But what can one expect from the Dutchies,
that had their peak with Automath in the 60s,
from then on it only went downhill.

Bye

Mild Shock schrieb:

Hi,

Instead presenting a clown world like here:

- The smart system for printing labels and reference
lines in Fitch proofs has been invented by B., a Prolog
expert who usually dislikes seeing his name quoted.
https://www.vidal-rosset.net/2025-11-17-swi-tinker-for-swi-prolog-provers.html


You could simply state that the Fitch renderer
is derived from Curry-Howard isomorphism proof
terms. This is pretty much folk knowledge in logic

circles, and wasnt invented by me. I was only
the messenger for things that every Logician should
know, already at least for 60 years, the original

THE FORMULAE-AS-TYPES NOTION OF CONSTRUCTION
W. A. Howard - University of Chicago
https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf

Curry-Howard paper already circulated in 1969.
That was around the same time when Automath
("automating mathematics") was devised by Nicolaas

Govert de Bruijn, for expressing complete mathematical
theories in such a way that an included automated
proof checker can verify their correctness.

Bye

Mild Shock schrieb:

Hi,

What if Computer Vision = Computer Linguistic.
That is, if the areas are based on the same
problems and the same solutions.

An example I rCLseerCY a doorknob.-a In order to
open the door I have to be able to visually
recognize a variety of different designs and
classify them according to function.

Is this part on the door intended to open the door?

We can do that as humans.-a It's the same problem
with words.-a There are different words with the
same "function" in a context. In principle it's

very similar, I could imagine that Computer Vision
has simply re-fertilized Computer Linguistic.

Bye

Mild Shock schrieb:

Hi,

How it started:

Computers Still Can't Do Beautiful Mathematics - by Gina Kolata
-----------------------------------------------------------------
Mathematicians often say that their craft is as much an art
as a science.-a But as more and more researchers are using
computers to prove their theorems, some worry that the magic
is in danger of fading away.

How its going:

Computers Do Produce Beautiful Mathematics - Dr. Larry Wos
-----------------------------------------------------------------
In addition to exhibiting logical reasoning of the type
found in mathematics, reasoning programs produce results
that are startling and elegant.-a Dr. J. Lukasiewicz was well
recognized for his contributions to areas of logic,

and yet the program OTTER recently found a proof far shorter and
more elegant than that produced by this eminent researcher,
and the program used the same notation and style of
reasoning.-a Mathematicians and logicians find elegance in
shorter proofs.

In August of 1990, Dr. Dana Scott of Carnegie Mellon
University attended a workshop at Argonne National
Laboratory.-a There he learned of OTTER and some of its uses
and successes.-a Upon returning to his university, Dr.
Scott's curiosity prompted him to suggest (via electronic
mail) 68 theorems for consideration by the computer.

His curiosity was almost immediately satisfied, for the sought-
after 68 proofs were returned with the comment that all were
obtained in a single computer run with the program--and in
less than 16 CPU minutes on a Sun 4 workstation.-a Dr. Scott
now uses his own copy of OTTER on his Macintosh.

Dr. R. Smullyan of the University of Indiana showed
great pleasure and surprise at learning of some of the
successes achieved by an automated reasoning program.-a As
evidence of his interest, he posed a number of questions,
receiving in turn the answers to all but one of them--a
question that is still open.
https://theory.stanford.edu/~uribe/mail/qed.messages/91.html

Bye

--- Synchronet 3.22a-Linux NewsLink 1.2