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

Groups > comp.lang.prolog > #14417

Secret Sauce of Dana Scott and Raymond Smullyan

Show all headers | View raw

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