Hi,--- Synchronet 3.21a-Linux NewsLink 1.2
Philosophy is a mandatory and highly important
subject in the French education system, studied
in the final year of high school (Terminale) and
as part of the Baccalauréat exams.
France has strong philosophy education but weak
interdisciplinary bridges, especially compared
to places like the US, UK, or Germany where
“logic” spans departments.
- Philosophers may focus on conceptual foundations,
argumentation, epistemology.
- Mathematicians/logicians focus on formal systems,
proof theory, model theory.
- Computer scientists focus on algorithms, computation,
complexity, type theory.
But see the positive side. You could write
a book about the glorious 1960s, that saw
the Curry-Howard theorem comming.
- The 1960s counterculture (“hippies”) were
drawn to new ways of thinking: systems, feedback loops,
interconnectedness — all ideas central to cybernetics.
- Netherlands-based logicians were quietly
inventing AUTOMATH and type theory. probably
visiting a coffee shop from time to time.
Bye
Hi,
Watch Alain Colmerauer juggle with 3 balls.
Thats the secret souce. Prolog is a circus.
Prologia cirque
Alain Colmerauer explique avec humour comment il
a dû jongler avec la recherche, l'enseignement et
l'entreprise ...cette vidéo a été filmée en VHS en
1994 à l'occasion de l'anniversaire de la création
de Prologia à Luminy, Marseille
https://www.youtube.com/watch?v=VyTgeUIb-OE
But it is usually not circus of clowns. It was many
times a circus of artists, that can juggle with Philosophy,
Mathematical Logic and Computer Science,
The contrary to morons like Boris the Loris,
Nazi Retard Julio, and many others, like EricGT,
Triska, Neumerkel, etc.. that forgot the roots of
Prolog, turning it into an ISO nonsense, or
Ciao with their "cause" of Prolog. Basically loosing
the Compass of Prolog.
Bye
Contact XLOG schrieb:
Hi,
Philosophy is a mandatory and highly important
subject in the French education system, studied
in the final year of high school (Terminale) and
as part of the Baccalauréat exams.
France has strong philosophy education but weak
interdisciplinary bridges, especially compared
to places like the US, UK, or Germany where
“logic” spans departments.
- Philosophers may focus on conceptual foundations,
argumentation, epistemology.
- Mathematicians/logicians focus on formal systems,
proof theory, model theory.
- Computer scientists focus on algorithms, computation,
complexity, type theory.
But see the positive side. You could write
a book about the glorious 1960s, that saw
the Curry-Howard theorem comming.
- The 1960s counterculture (“hippies”) were
drawn to new ways of thinking: systems, feedback loops,
interconnectedness — all ideas central to cybernetics.
- Netherlands-based logicians were quietly
inventing AUTOMATH and type theory. probably
visiting a coffee shop from time to time.
Bye
Hi,
Somebody attributed to me:
"The smart system to print via Prolog labels
and reference lines in Fitch proofs"
But you find the Fitch labeling already here:
Rewriting for Fitch Style Natural Deductions
Herman Geuvers, Rob-Nederpelt - 2004 https://www.researchgate.net/publication/221220647
Bye
P.S.: I had a lot of smart posted on SWI-Prolog
discourse, an other post had a few tricks to
nicely render proofs involving quantifiers.
Still I was scolded and laughed at. At one
moment the silly Philosophy Professor asked
whether I am even human. What is the result
of this ignorance. A prover that doesn't work.
I first thought I would do some fuzzy testing.
But then I hand picked a manuel example from
FOL and not from propositional logic:
?- prove(?[X]:(d(X) => ![Y]:d(Y))). https://en.wikipedia.org/wiki/Drinker_paradox
It doesn't produce something useful, although
it says it has found a proof:
Continue despite warnings? (y/n): |: y. ------------------------------------------
G4 PROOF FOR: ?[_4012-_4014]:(d(_4012-_4014)=>![_3560]:d(_3560)) ------------------------------------------
MODE: Theorem
=== CLASSICAL PATTERN DETECTED ===
-> Skipping constructive logic
=== TRYING CLASSICAL LOGIC ===
% 210 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
Classical proof found
G4+IP proofs in classical logic
- Sequent Calculus -
\begin{prooftree}
\AxiomC{}
\RightLabel{\scriptsize{$Ax.$}}
\UnaryInfC{$
false.
Was the thingy even tested before it went online? https://swi-prolog.discourse.group/t/swi-tinker-for-g4-mic-f-o-l-automated-prover/9410
Mild Shock schrieb:
Hi,
Watch Alain Colmerauer juggle with 3 balls.
Thats the secret souce. Prolog is a circus.
Prologia cirque
Alain Colmerauer explique avec humour comment il
a dû jongler avec la recherche, l'enseignement et
l'entreprise ...cette vidéo a été filmée en VHS en
1994 à l'occasion de l'anniversaire de la création
de Prologia à Luminy, Marseille
https://www.youtube.com/watch?v=VyTgeUIb-OE
But it is usually not circus of clowns. It was many
times a circus of artists, that can juggle with Philosophy,
Mathematical Logic and Computer Science,
The contrary to morons like Boris the Loris,
Nazi Retard Julio, and many others, like EricGT,
Triska, Neumerkel, etc.. that forgot the roots of
Prolog, turning it into an ISO nonsense, or
Ciao with their "cause" of Prolog. Basically loosing
the Compass of Prolog.
Bye
Contact XLOG schrieb:
Hi,
;
Philosophy is a mandatory and highly important
subject in the French education system, studied
in the final year of high school (Terminale) and
as part of the Baccalauréat exams.
;
France has strong philosophy education but weak
interdisciplinary bridges, especially compared
to places like the US, UK, or Germany where
“logic” spans departments.
;
- Philosophers may focus on conceptual foundations,
argumentation, epistemology.
- Mathematicians/logicians focus on formal systems,
proof theory, model theory.
- Computer scientists focus on algorithms, computation,
complexity, type theory.
;
But see the positive side. You could write
a book about the glorious 1960s, that saw
the Curry-Howard theorem comming.
;
- The 1960s counterculture (“hippies”) were
drawn to new ways of thinking: systems, feedback loops,
interconnectedness — all ideas central to cybernetics.
;
- Netherlands-based logicians were quietly
inventing AUTOMATH and type theory. probably
visiting a coffee shop from time to time.
;
Bye
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
Me: LEM is derivable from RAA, in minimal logic.
Prof: LEM is not even derivable from RAA in intuitionistic logic.
Me: You didn’t 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 didn’t 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 \lnot A)$}
\RightLabel{\scriptsize{$ \lor\to E$}}
\UnaryInfC{$ \lnot \lnot A$}
\AxiomC{\scriptsize{1}}
\noLine
\UnaryInfC{$ \lnot (A \lor \lnot A)$}
\RightLabel{\scriptsize{$ \lor\to E$}}
\UnaryInfC{$ \lnot A$}
\RightLabel{\scriptsize{$ \to E $}}
\BinaryInfC{$\bot$}
\RightLabel{\scriptsize{$ IP $} 1}
\UnaryInfC{$A \lor \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. 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: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,089 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 153:45:51 |
| Calls: | 13,921 |
| Calls today: | 2 |
| Files: | 187,021 |
| D/L today: |
3,746 files (943M bytes) |
| Messages: | 2,457,162 |