From Newsgroup: comp.lang.prolog

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 “see” a doorknob.  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.  It's the same problem
with words.  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.  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.  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.  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.  There he learned of OTTER and some of its uses
and successes.  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.  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.  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.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

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 “see” a doorknob.  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.  It's the same problem
with words.  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.  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.  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.  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.  There he learned of OTTER and some of its uses
and successes.  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.  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.  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.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

Hi,

Now I found this Coq gem from 2020,
it uses a server roundtrip to render
stuff in the web:

Alectryon: Untangling Mechanized Proofs
Clément Pit-Claudel - SLE 2020
https://dl.acm.org/doi/10.1145/3426425.3426940

It predates Dogelog Player , and it
also predates SWI-Tinker. I am pretty
sure without the server roundtrip something

much more animated can be done. For example
not only visualize the evolution of various
configurations of Conway’s Game of Life,

but have Conway's Game of Life run in the browser.
But the pains are very big. Take Fitch style
rendering, this is Long Life Learning L^3

experience, emerited professors such as Joseph
Vidal Rosset have still the chance to grok
Howard Curry, before they bite the dust.

But is nowadays L^3 even a good model of
societal growth? I suspect Stable Diffusion
can pick up and incorporate Proof Rendering

as well, and we might just subsume everythinbg
via Generative AI. I have already seen cute
racoons generated on my laptop which is a Copilot+

enabled laptop, that can perform Local AI.

Bye

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 “see” a doorknob.  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.  It's the same problem
with words.  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.  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.  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.  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.  There he learned of OTTER and some of its uses
and successes.  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.  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.  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.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog


"considered consequence". Ha Ha, why this
formulation? I voluntarily used the Curry-
Howard theorem, when I developed my Prolog

code. I didn't invent anything. And its not
a smart system. Please never use the word
"smart" in software engineering, thats not

professional. In particular the Implication
Introduction rule has been documented around
the world a 100x times: Just have a look:

Intuitionistic implicational natural deduction

G, A |- B
------------ (->I)
G |- A -> B

Lambda calculus type assignment rules

G, x:A |- t:B
----------------------- (->I)
G |- (λx:A.t) : A -> B

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_natural_deduction_and_typed_lambda_calculus

Also refering to the above is probably more
useful, than referning to the paper. Since
it gives a summary of propositional

MINIMAL LOGIC in Curry-Howard simple types.

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

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

Hi,

Don't worry, be happy: Take your time.
Maybe the matter rings a bell in 1, 2
or 5 years. Who knows?

Or even better, in 3, 6 or 12 months.
Maybe France has somewhere a library
with a book about Type Theory?

Or if all else fails try knocking on
the doors of INRIA, a friendly student
might appear, and explain the

matter face 2 face, in a few minutes.

Bye

Mild Shock schrieb:

"considered consequence". Ha Ha, why this
formulation? I voluntarily used the Curry-
Howard theorem, when I developed my Prolog

code. I didn't invent anything. And its not
a smart system. Please never use the word
"smart" in software engineering, thats not

professional. In particular the Implication
Introduction rule has been documented around
the world a 100x times: Just have a look:

Intuitionistic implicational natural deduction

G, A |- B
------------ (->I)
G |- A -> B

Lambda calculus type assignment rules

G, x:A |- t:B
----------------------- (->I)
G |- (λx:A.t) : A -> B

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_natural_deduction_and_typed_lambda_calculus

Also refering to the above is probably more
useful, than referning to the paper. Since
it gives a summary of propositional

MINIMAL LOGIC in Curry-Howard simple types.

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

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

Hi,

Philosophy is a mandatory and highly important
subject in the French education system, studied
in the final year of high school (Terminale) and
as part of the Baccalauréat exams.

France has strong philosophy education but weak
interdisciplinary bridges, especially compared
to places like the US, UK, or Germany where
“logic” spans departments.

- Philosophers may focus on conceptual foundations,
argumentation, epistemology.
- Mathematicians/logicians focus on formal systems,
proof theory, model theory.
- Computer scientists focus on algorithms, computation,
complexity, type theory.

But see the positive side. You could write
a book about the glorious 1960s, that saw
the Curry-Howard theorem comming.

- The 1960s counterculture (“hippies”) were
drawn to new ways of thinking: systems, feedback loops,
interconnectedness — all ideas central to cybernetics.

- Netherlands-based logicians were quietly
inventing AUTOMATH and type theory. probably
visiting a coffee shop from time to time.

Bye

Mild Shock schrieb:

Hi,

Don't worry, be happy: Take your time.
Maybe the matter rings a bell in 1, 2
or 5 years. Who knows?

Or even better, in 3, 6 or 12 months.
Maybe France has somewhere a library
with a book about Type Theory?

Or if all else fails try knocking on
the doors of INRIA, a friendly student
might appear, and explain the

matter face 2 face, in a few minutes.

Bye

Mild Shock schrieb:

"considered consequence". Ha Ha, why this
formulation? I voluntarily used the Curry-
Howard theorem, when I developed my Prolog

code. I didn't invent anything. And its not
a smart system. Please never use the word
"smart" in software engineering, thats not

professional. In particular the Implication
Introduction rule has been documented around
the world a 100x times: Just have a look:

Intuitionistic implicational natural deduction

G, A |- B
------------ (->I)
G |- A -> B

Lambda calculus type assignment rules

G, x:A |- t:B
----------------------- (->I)
G |- (λx:A.t) : A -> B

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_natural_deduction_and_typed_lambda_calculus


Also refering to the above is probably more
useful, than referning to the paper. Since
it gives a summary of propositional

MINIMAL LOGIC in Curry-Howard simple types.

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

--- Synchronet 3.21a-Linux NewsLink 1.2