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

Groups > comp.lang.prolog > #15122

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

Show all headers | View raw

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

Back to comp.lang.prolog | Previous | Next — Previous in thread | 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