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.-a 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.-a 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.-a 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.-a There he learned of OTTER and some of its uses
and successes.-a 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.-a 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.-a 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
Me: LEM is derivable from RAA, in minimal logic.
Prof: LEM is not even derivable from RAA in intuitionistic logic.
Me: You didnrCOt use RAA as an inference schema!
Prof: Our discussion is about logic and not about Prolog. I apologize.
Hi,
I always admired the French Teaching of Logic.
This silly Philosophy Professor scolded me a couple
of times with this nonsense, playing dumb and deaf,
like a complete idiot:
Me: LEM is derivable from RAA, in minimal logic.
Prof: LEM is not even derivable from RAA in intuitionistic logic.
Me: You didnrCOt use RAA as an inference schema!
Prof: Our discussion is about logic and not about Prolog. I apologize. https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/78
Still his prover demonstrates LEM from RAA:
?-prove((a | ~a)).
\begin{prooftree}
\AxiomC{\scriptsize{1}}
\noLine
\UnaryInfC{$ \lnot (A \lor-a \lnot A)$}
\RightLabel{\scriptsize{$ \lor\to E$}}
\UnaryInfC{$ \lnot-a \lnot A$}
\AxiomC{\scriptsize{1}}
\noLine
\UnaryInfC{$ \lnot (A \lor-a \lnot A)$}
\RightLabel{\scriptsize{$ \lor\to E$}}
\UnaryInfC{$ \lnot A$}
\RightLabel{\scriptsize{$ \to E $}}
\BinaryInfC{$\bot$}
\RightLabel{\scriptsize{$ IP $}-a 1}
\UnaryInfC{$A \lor-a \lnot A$}
\end{prooftree} https://g4-mic.vidal-rosset.net/wasm/tinker#prove((a%20%7C%20~a)).
Please note that RAA = IP, synonymous names.
Reductio Ad Absurdum and Indirect Proof.
LoL
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.-a 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.-a 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.-a 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.-a There he learned of OTTER and some of its uses
and successes.-a 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.-a 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.-a 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: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 54 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 19:03:52 |
| Calls: | 742 |
| Files: | 1,218 |
| D/L today: |
5 files (8,203K bytes) |
| Messages: | 184,913 |
| Posted today: | 1 |