Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.prolog > #15116

The SWI-Prolog community is a circus (Was: The Clown World of Joseph Vidal Rosset)

Show all headers | View raw

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

Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Secret Sauce of Dana Scott and Raymond Smullyan Mild Shock <janburse@fastmail.fm> - 2025-01-18 01:15 +0100
  The Clown World of Joseph Vidal Rosset (Re: Philosophize not God, Philosophize the Door Knob) Mild Shock <janburse@fastmail.fm> - 2025-12-04 11:26 +0100
    The SWI-Prolog community is a circus (Was: The Clown World of Joseph Vidal Rosset) Mild Shock <janburse@fastmail.fm> - 2025-12-04 11:47 +0100
      Alectryon: Long Life Learning or Stable Diffusion? (Was: The SWI-Prolog community is a circus) Mild Shock <janburse@fastmail.fm> - 2025-12-04 13:37 +0100
      From Unrusting Blade to Unburning Icarus (Re: The SWI-Prolog community is a circus ) Mild Shock <janburse@fastmail.fm> - 2026-07-27 12:18 +0200
    "considered consequence". Ha Ha, why this formulation? (Was: The Clown World of Joseph Vidal Rosset) Mild Shock <janburse@fastmail.fm> - 2025-12-04 21:41 +0100
      Don't worry, be happy: Take your time (Re: "considered consequence". Ha Ha, why this formulation?) Mild Shock <janburse@fastmail.fm> - 2025-12-04 21:57 +0100
        Write a book about the glorious 1960s (Re: Don't worry, be happy: Take your time) Mild Shock <janburse@fastmail.fm> - 2025-12-04 22:40 +0100
  Alain Colmerauer: Prologia cirque (Re: Secret Sauce of Dana Scott and Raymond Smullyan) Mild Shock <janburse@fastmail.fm> - 2025-12-04 22:52 +0100
    Where did the "smarts" go? Drinker Paradox fails (Was: Alain Colmerauer: Prologia cirque) Mild Shock <janburse@fastmail.fm> - 2025-12-05 15:46 +0100
      BB(N): Prover should be verified [Henkin Constructive?] (Was: Where did the "smarts" go? Drinker Paradox fails) Mild Shock <janburse@fastmail.fm> - 2025-12-05 16:08 +0100
  The French Square Wheele Bicycle of Logic (Re: Secret Sauce of Dana Scott and Raymond Smullyan) Mild Shock <janburse@fastmail.fm> - 2025-12-05 19:54 +0100
    The episode told everything about the Character (Re: The French Square Wheele Bicycle of Logic) Mild Shock <janburse@fastmail.fm> - 2025-12-05 20:12 +0100

csiph-web