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

Groups > comp.lang.prolog > #15115

The Clown World of Joseph Vidal Rosset (Re: Philosophize not God, Philosophize the Door Knob)

Show all headers | View raw

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