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
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
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 475 |
| Nodes: | 16 (3 / 13) |
| Uptime: | 147:23:18 |
| Calls: | 9,477 |
| Calls today: | 8 |
| Files: | 13,610 |
| Messages: | 6,120,733 |