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

Groups > comp.lang.prolog > #14417 > unrolled thread

Secret Sauce of Dana Scott and Raymond Smullyan

Back to article view | Back to comp.lang.prolog

Contents

  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

#14417 — Secret Sauce of Dana Scott and Raymond Smullyan

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

[toc] | [next] | [standalone]

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

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
> 

[toc] | [prev] | [next] | [standalone]

#15116 — The SWI-Prolog community is a circus (Was: The Clown World of Joseph Vidal Rosset)

Hi,

The SWI-Prolog community is a circus.
I mean there are not only clowns like
Boris the Loris and Nazi Retard Julio,

there are also clowns like completely
mentally deranged Philosophy Professors,
such as Joseph Vidal Rosset.

But what can one expect from the Dutchies,
that had their peak with Automath in the 60s,
from then on it only went downhill.

Bye

Mild Shock schrieb:
> 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
>>
> 

[toc] | [prev] | [next] | [standalone]

#15117 — Alectryon: Long Life Learning or Stable Diffusion? (Was: The SWI-Prolog community is a circus)

Hi,

Now I found this Coq gem from 2020,
it uses a server roundtrip to render
stuff in the web:

Alectryon: Untangling Mechanized Proofs
Clément Pit-Claudel - SLE 2020
https://dl.acm.org/doi/10.1145/3426425.3426940

It predates Dogelog Player , and it
also predates SWI-Tinker. I am pretty
sure without the server roundtrip something

much more animated can be done. For example
not only visualize the evolution of various
configurations of Conway’s Game of Life,

but have Conway's Game of Life run in the browser.
But the pains are very big. Take Fitch style
rendering, this is Long Life Learning L^3

experience, emerited professors such as Joseph
Vidal Rosset have still the chance to grok
Howard Curry, before they bite the dust.

But is nowadays L^3 even a good model of
societal growth? I suspect Stable Diffusion
can pick up and incorporate Proof Rendering

as well, and we might just subsume everythinbg
via Generative AI. I have already seen cute
racoons generated on my laptop which is a Copilot+

enabled laptop, that can perform Local AI.

Bye

Mild Shock schrieb:
> Hi,
> 
> The SWI-Prolog community is a circus.
> I mean there are not only clowns like
> Boris the Loris and Nazi Retard Julio,
> 
> there are also clowns like completely
> mentally deranged Philosophy Professors,
> such as Joseph Vidal Rosset.
> 
> But what can one expect from the Dutchies,
> that had their peak with Automath in the 60s,
> from then on it only went downhill.
> 
> Bye
> 
> Mild Shock schrieb:
>> 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
>>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#15753 — From Unrusting Blade to Unburning Icarus (Re: The SWI-Prolog community is a circus )

Hi,

Now the SWI community has create a new circus
example, probably AI generated by a prompt
enginerring, add a silly greeting line:

A: Thank you so much for sharing information
    about the LogicBiz V.2.0 project!
B: Thank you so much for your kind words
    and encouragement!
A: Thank you so much for your honest and
    heartfelt reply!
B: Thank you so much for your heartwarming
    and supportive reply!
A: Thank you for your openness!
B: Thank you for your valuable feedback!
A: Thank you for sharing such a detailed
    and impressive technical breakdown!
B: Thank you for the detailed breakdown!
A: Thank you for the fascinating perspective!
https://swi-prolog.discourse.group/t/the-unrusting-blade-an-offline-first-logicbiz-v-2-0-powered-by-swi-prolog-sqlcipher-reply-01/9752

The pinacle of their "logic programming":

"Barcode Scanners & EDC inputs: Barcode scanners
inherently act as Human Interface Devices (HID) —
meaning they just inject keyboard strokes into
the active field. Since my input terminal is
already standard web HTML, a physical USB/Bluetooth
scanner works instantly out-of-the-box without
needing complex C/C++ bindings or custom drivers
in Prolog. The same applies to manually
entering EDC trace codes."
https://swi-prolog.discourse.group/t/the-unrusting-blade-an-offline-first-logicbiz-v-2-0-powered-by-swi-prolog-sqlcipher-reply-01/9752

Thank you for your unhinged nonsense!

Bye

P.S.: Isn't following georgi gerganov or
andrej karpathy more exciting. What if you
want to integrate a chatbot into your web

storefront, which is not a point of sale,
but a pizza ordering web site? Do it with
uber eats out of the box. Are we already lost?

Or can we rise without burning?

Mild Shock schrieb:
> Hi,
> 
> The SWI-Prolog community is a circus.
> I mean there are not only clowns like
> Boris the Loris and Nazi Retard Julio,
> 
> there are also clowns like completely
> mentally deranged Philosophy Professors,
> such as Joseph Vidal Rosset.
> 
> But what can one expect from the Dutchies,
> that had their peak with Automath in the 60s,
> from then on it only went downhill.
> 
> Bye
> 
> Mild Shock schrieb:
>> 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
>>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#15118 — "considered consequence". Ha Ha, why this formulation? (Was: The Clown World of Joseph Vidal Rosset)

"considered consequence". Ha Ha, why this
formulation? I voluntarily used the Curry-
Howard theorem, when I developed my Prolog

code. I didn't invent anything. And its not
a smart system. Please never use the word
"smart" in software engineering, thats not

professional. In particular the Implication
Introduction rule has been documented around
the world a 100x times: Just have a look:

Intuitionistic implicational natural deduction

G, A |- B
------------ (->I)
G |- A -> B

Lambda calculus type assignment rules

G, x:A |- t:B
----------------------- (->I)
G |- (λx:A.t) : A -> B

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_natural_deduction_and_typed_lambda_calculus

Also refering to the above is probably more
useful, than referning to the paper. Since
it gives a summary of propositional

MINIMAL LOGIC in Curry-Howard simple types.

Mild Shock schrieb:
> 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

[toc] | [prev] | [next] | [standalone]

#15119 — Don't worry, be happy: Take your time (Re: "considered consequence". Ha Ha, why this formulation?)

Hi,

Don't worry, be happy: Take your time.
Maybe the matter rings a bell in 1, 2
or 5 years. Who knows?

Or even better, in 3, 6 or 12 months.
Maybe France has somewhere a library
with a book about Type Theory?

Or if all else fails try knocking on
the doors of INRIA, a friendly student
might appear, and explain the

matter face 2 face, in a few minutes.

Bye

Mild Shock schrieb:
> 
> "considered consequence". Ha Ha, why this
> formulation? I voluntarily used the Curry-
> Howard theorem, when I developed my Prolog
> 
> code. I didn't invent anything. And its not
> a smart system. Please never use the word
> "smart" in software engineering, thats not
> 
> professional. In particular the Implication
> Introduction rule has been documented around
> the world a 100x times: Just have a look:
> 
> Intuitionistic implicational natural deduction
> 
> G, A |- B
> ------------ (->I)
> G |- A -> B
> 
> Lambda calculus type assignment rules
> 
> G, x:A |- t:B
> ----------------------- (->I)
> G |- (λx:A.t) : A -> B
> 
> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_natural_deduction_and_typed_lambda_calculus 
> 
> 
> Also refering to the above is probably more
> useful, than referning to the paper. Since
> it gives a summary of propositional
> 
> MINIMAL LOGIC in Curry-Howard simple types.
> 
> Mild Shock schrieb:
>> 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
> 
> 

[toc] | [prev] | [next] | [standalone]

#15120 — Write a book about the glorious 1960s (Re: Don't worry, be happy: Take your time)

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

Mild Shock schrieb:
> Hi,
> 
> Don't worry, be happy: Take your time.
> Maybe the matter rings a bell in 1, 2
> or 5 years. Who knows?
> 
> Or even better, in 3, 6 or 12 months.
> Maybe France has somewhere a library
> with a book about Type Theory?
> 
> Or if all else fails try knocking on
> the doors of INRIA, a friendly student
> might appear, and explain the
> 
> matter face 2 face, in a few minutes.
> 
> Bye
> 
> Mild Shock schrieb:
>>
>> "considered consequence". Ha Ha, why this
>> formulation? I voluntarily used the Curry-
>> Howard theorem, when I developed my Prolog
>>
>> code. I didn't invent anything. And its not
>> a smart system. Please never use the word
>> "smart" in software engineering, thats not
>>
>> professional. In particular the Implication
>> Introduction rule has been documented around
>> the world a 100x times: Just have a look:
>>
>> Intuitionistic implicational natural deduction
>>
>> G, A |- B
>> ------------ (->I)
>> G |- A -> B
>>
>> Lambda calculus type assignment rules
>>
>> G, x:A |- t:B
>> ----------------------- (->I)
>> G |- (λx:A.t) : A -> B
>>
>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Intuitionistic_natural_deduction_and_typed_lambda_calculus 
>>
>>
>> Also refering to the above is probably more
>> useful, than referning to the paper. Since
>> it gives a summary of propositional
>>
>> MINIMAL LOGIC in Curry-Howard simple types.
>>
>> Mild Shock schrieb:
>>> 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
>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#15121 — Alain Colmerauer: Prologia cirque (Re: Secret Sauce of Dana Scott and Raymond Smullyan)

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

[toc] | [prev] | [next] | [standalone]

#15122 — Where did the "smarts" go? Drinker Paradox fails (Was: Alain Colmerauer: Prologia cirque)

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

[toc] | [prev] | [next] | [standalone]

#15123 — BB(N): Prover should be verified [Henkin Constructive?] (Was: Where did the "smarts" go? Drinker Paradox fails)

Hi,

Well the problem might be only the rendering.
Ultimately a prover itself should be verified.
The Isabelle/HOL people did that for SAT solvers:

A Verified SAT Solver Framework
Jasmin Christian Blanchette et. al. 2018
https://matryoshka-project.github.io/pubs/sat_article.pdf

What would be a funny project, to refrain from
using infinite actual sets. Do a Gödel completeness
proof with infinite potential sets, applying

a kind of Scott's trick, maybe it would make the
proof even amenable to be carried out in the prover
itself, that is verified, requireing only a little

theory, like for example Kőnig's lemma. Henkin
model proofs are not really constructive. The involve
a choice among A v ~A. The problem is when constructing

a model, adding a literal A or ~A could lead in both
cases to a consistent new theory. It would be easier
when one of the literatals A or ~A would lead to

an inconsistency, giving a kind of choice certificate.
But the choice is kind of uncertified, in the
forcing for Henkin models. Not sure whether it can

be made a little bit more constructive. It also
relates to the busy beaver discussion, the recent
result that BB(748) is independent of ZFC.

Bye

Mild Shock schrieb:
> 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
> 

[toc] | [prev] | [next] | [standalone]

#15126 — The French Square Wheele Bicycle of Logic (Re: Secret Sauce of Dana Scott and Raymond Smullyan)

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

[toc] | [prev] | [next] | [standalone]

#15127 — The episode told everything about the Character (Re: The French Square Wheele Bicycle of Logic)

Hi,

The episode told me everything about the Character
of the silly Philosophy Professor:

 > 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

There were similar episodes, on the SWI-Prolog discourse
forum. In the same style. So there is no loss that I cannot

post anymore on SWI-Prolog discourse. But please:

*NEVER EVER CITE ME IN YOUR WORK*

Bye

Mild Shock schrieb:
> 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
> 

[toc] | [prev] | [standalone]

Back to top | Article view | comp.lang.prolog

csiph-web