From Newsgroup: comp.lang.prolog

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 |a l'occasion de l'anniversaire de la cr|-ation
de Prologia |a 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
rCLlogicrCY 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 (rCLhippiesrCY) were
drawn to new ways of thinking: systems, feedback loops,
interconnectedness rCo 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

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

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 |a l'occasion de l'anniversaire de la cr|-ation
de Prologia |a 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
rCLlogicrCY 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 (rCLhippiesrCY) were
drawn to new ways of thinking: systems, feedback loops,
interconnectedness rCo 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

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

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+anig'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 ===
-a-a-a -> Skipping constructive logic
=== TRYING CLASSICAL LOGIC ===
% 210 inferences, 0.000 CPU in 0.000 seconds (?% CPU, Infinite Lips)
-a-a 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 |a l'occasion de l'anniversaire de la cr|-ation
de Prologia |a 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
rCLlogicrCY 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 (rCLhippiesrCY) were
drawn to new ways of thinking: systems, feedback loops,
interconnectedness rCo 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

--- Synchronet 3.21a-Linux NewsLink 1.2