info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Proposal for a proof assistants StackExchange site
313 views
Skip to first unread message
FredJeffries
Nov 19, 2021, 8:44:40 PM11/19/21
to
Andrej Bauer has created a proposal for a new 'Proof assistants' StackExchange site.
http://math.andrej.com/2021/11/20/proof-assistants-stackexchange-site/
https://area51.stackexchange.com/proposals/126242/proof-assistants
http://math.andrej.com/2021/11/20/proof-assistants-stackexchange-site/
https://area51.stackexchange.com/proposals/126242/proof-assistants
Mostowski Collapse
Nov 19, 2021, 9:36:50 PM11/19/21
to
Never ever put your soul on stack exchange. They will not only
disown you quickly, you will also not be able to deleted it. The have
implemented technical means to block you from deleting your own content.
From their terms and conditions:
https://stackoverflow.com/legal/terms-of-service#licensing
"Subscriber Content
You agree that any and all content, including without limitation
any and all text, graphics, logos, tools, photographs, images,
illustrations, software or source code, audio and video, animations,
and product feedback (collectively, “Content”) that you provide to
the public Network (collectively, “Subscriber Content”), is perpetually
and irrevocably licensed to Stack Overflow on a worldwide, royalty-free,
non-exclusive basis pursuant to Creative Commons licensing terms
(CC BY-SA 4.0), and you grant Stack Overflow the perpetual and
irrevocable right and license to access, use, process, copy, distribute,
export, display and to commercially exploit such Subscriber Content,
even if such Subscriber Content has been contributed and subsequently
removed by you as reasonably necessary to, for example (without limitation):
Provide, maintain, and update the public Network
Process lawful requests from law enforcement agencies and government agencies
Prevent and address security incidents and data security features,
support features, and to provide technical assistance as it may be required
Aggregate data to provide product optimization
This means that you cannot revoke permission for Stack Overflow
to publish, distribute, store and use such content and to allow others
to have derivative rights to publish, distribute, store and use such
content. The CC BY-SA 4.0 license terms are explained in further
detail by Creative Commons, and the license terms applicable to
content are explained in further detail here. You should be aware
that all Public Content you contribute is available for public copy
and redistribution, and all such Public Content must have
appropriate attribution."
disown you quickly, you will also not be able to deleted it. The have
implemented technical means to block you from deleting your own content.
From their terms and conditions:
https://stackoverflow.com/legal/terms-of-service#licensing
"Subscriber Content
You agree that any and all content, including without limitation
any and all text, graphics, logos, tools, photographs, images,
illustrations, software or source code, audio and video, animations,
and product feedback (collectively, “Content”) that you provide to
the public Network (collectively, “Subscriber Content”), is perpetually
and irrevocably licensed to Stack Overflow on a worldwide, royalty-free,
non-exclusive basis pursuant to Creative Commons licensing terms
(CC BY-SA 4.0), and you grant Stack Overflow the perpetual and
irrevocable right and license to access, use, process, copy, distribute,
export, display and to commercially exploit such Subscriber Content,
even if such Subscriber Content has been contributed and subsequently
removed by you as reasonably necessary to, for example (without limitation):
Provide, maintain, and update the public Network
Process lawful requests from law enforcement agencies and government agencies
Prevent and address security incidents and data security features,
support features, and to provide technical assistance as it may be required
Aggregate data to provide product optimization
This means that you cannot revoke permission for Stack Overflow
to publish, distribute, store and use such content and to allow others
to have derivative rights to publish, distribute, store and use such
content. The CC BY-SA 4.0 license terms are explained in further
detail by Creative Commons, and the license terms applicable to
content are explained in further detail here. You should be aware
that all Public Content you contribute is available for public copy
and redistribution, and all such Public Content must have
appropriate attribution."
Mostowski Collapse
Nov 19, 2021, 9:46:26 PM11/19/21
to
The most annoying thing is that the administrators use
a ticket system, and in principle they make legally binding
promisses, only they don't care what kind of promisses they
write as answers into their own ticket system, the next
day they change their mind, and do something else. So
you cannot trust their word, because the rights you give
them, in principle they need not be executed. But like
the birtish museum has more mummies than Egypt itself,
the stackexchange have more irrelevant information
about your long retracted project than you would ever
dream of. The way back machine has even not that much
outdated nonsense in store. Even the house of a messie
looks clean compared to stack exchange sites.
a ticket system, and in principle they make legally binding
promisses, only they don't care what kind of promisses they
write as answers into their own ticket system, the next
day they change their mind, and do something else. So
you cannot trust their word, because the rights you give
them, in principle they need not be executed. But like
the birtish museum has more mummies than Egypt itself,
the stackexchange have more irrelevant information
about your long retracted project than you would ever
dream of. The way back machine has even not that much
outdated nonsense in store. Even the house of a messie
looks clean compared to stack exchange sites.
Mostowski Collapse
Nov 19, 2021, 10:01:52 PM11/19/21
to
Also they swim in money:
https://arstechnica.com/gadgets/2021/06/stack-overflow-sold-to-tech-investor-prosus-for-1-8-billion/
But they can even not make a syntax highlighter
that works correctly for the Prolog programming
language, and laugh at you when you request that.
You also wont see a bit of this money in your own
poket. The only incentive they offer is their gamefication
of Q & A, and astonishingly for many that seems to
be motivation. They only use you to earn more money
with their job fair spin off etc.. etc.. and the content has
become click bait for job offers. Because of this degradation
of their content, for many problems you now find much
better sites and much better courated information.
Typically problems are now also addressed by YouTubers
etc.., because others want also profit from this Q & A
traffic magnet. It is quite likely that stack exchanges will
disappear if their bit rot continues as it does now.
https://arstechnica.com/gadgets/2021/06/stack-overflow-sold-to-tech-investor-prosus-for-1-8-billion/
But they can even not make a syntax highlighter
that works correctly for the Prolog programming
language, and laugh at you when you request that.
You also wont see a bit of this money in your own
poket. The only incentive they offer is their gamefication
of Q & A, and astonishingly for many that seems to
be motivation. They only use you to earn more money
with their job fair spin off etc.. etc.. and the content has
become click bait for job offers. Because of this degradation
of their content, for many problems you now find much
better sites and much better courated information.
Typically problems are now also addressed by YouTubers
etc.., because others want also profit from this Q & A
traffic magnet. It is quite likely that stack exchanges will
disappear if their bit rot continues as it does now.
Mostowski Collapse
Nov 19, 2021, 10:23:13 PM11/19/21
to
About Zulip I don't know. Somehow the gameification stack
exchange rule system does not guarantee high quality,
because it is more based on hunters and collectors mentality,
where everything is taken and infinitely kept. On a first
sight the rational makes sense, especially for example for
computer related stuff. I might quite well have an Amiga
at home, and ask a question about it. But is this true? There
is rather a trend now to quickly move one, and eradicate
old releases, move them out of circulation. Outdated stuff
that gets stuck in wild only generates cost. It might be full
of security holes, or shows long dismissed behaviour, because
some specs have evolved. Stack exchange was designed
without the concept of end of lifetime in mind. This shines.
If you try to pull the plug of something, and by accident you
hit some alarm threshold, its impossible to explain an admistrator
that you need an excepgt. The admistrators have become
robots, that are not able to question the rules of their system.
If you would employ them in Auschwitz, they would efficiently
gas people after people. They have become brainless bricks.
exchange rule system does not guarantee high quality,
because it is more based on hunters and collectors mentality,
where everything is taken and infinitely kept. On a first
sight the rational makes sense, especially for example for
computer related stuff. I might quite well have an Amiga
at home, and ask a question about it. But is this true? There
is rather a trend now to quickly move one, and eradicate
old releases, move them out of circulation. Outdated stuff
that gets stuck in wild only generates cost. It might be full
of security holes, or shows long dismissed behaviour, because
some specs have evolved. Stack exchange was designed
without the concept of end of lifetime in mind. This shines.
If you try to pull the plug of something, and by accident you
hit some alarm threshold, its impossible to explain an admistrator
that you need an excepgt. The admistrators have become
robots, that are not able to question the rules of their system.
If you would employ them in Auschwitz, they would efficiently
gas people after people. They have become brainless bricks.
Mostowski Collapse
Nov 19, 2021, 10:34:09 PM11/19/21
to
The "end of lifetime" concept is very common now
in computers, but it is for example alien to mathematics.
Pythagoras theorem is an ethernal thruth, it doesnt have
an "end of lifetime". But if you do proof assistants, you
will again deal with computers. So a Q & A site that
cannot handle "end of lifetime" would be a pain in
the ass. Some computer projects keep long records
of everything, for example python, has quite a big collection
of PEPs. But then their might be revolutions, like going
from python2 to python3, and things become versioned.
Stack exchange is too stupid to offer something that
would have a similar effect. They have "tags". I tried
marking the outdated stuff by a "tag", but there were
the following limitations:
- Question can only have maximally 5 tags
- Answers do not have tags at all!
So I gave up and deleted my account. Now my account
is dissassociated from all questions and answers,
and the question and answers are a big mess, and talk
about a Prolog system that doesn't exist anymore.
LoL
Stack exchange is just a joke!
in computers, but it is for example alien to mathematics.
Pythagoras theorem is an ethernal thruth, it doesnt have
an "end of lifetime". But if you do proof assistants, you
will again deal with computers. So a Q & A site that
cannot handle "end of lifetime" would be a pain in
the ass. Some computer projects keep long records
of everything, for example python, has quite a big collection
of PEPs. But then their might be revolutions, like going
from python2 to python3, and things become versioned.
Stack exchange is too stupid to offer something that
would have a similar effect. They have "tags". I tried
marking the outdated stuff by a "tag", but there were
the following limitations:
- Question can only have maximally 5 tags
- Answers do not have tags at all!
So I gave up and deleted my account. Now my account
is dissassociated from all questions and answers,
and the question and answers are a big mess, and talk
about a Prolog system that doesn't exist anymore.
LoL
Stack exchange is just a joke!
Mostowski Collapse
Nov 20, 2021, 9:34:51 AM11/20/21
to
Also I wouldn't trust Andrej Bauer when he sets up such
a group. He can be quite "posh", for example he cancels
people on cs.stackexchange.com, because he claims
the question is not a research question. And then
he finds support for this cancel culture by the charter
of cs.stackexchange.com. So stack exchange sites
are known to implement a form of class racism. There
is a danger that this proof assistant stack exchange site
not only becomes a bitrot exchange, but also
those pieces that are not bitrot do not become accessible
to all, and not everybody can contribute. So it might become
an elite thing like mathoverflow, cs.stackexchange.com, etc..
but logic and set theory for example, should be available
to everyone. Especially via tools they should provide end-user
empowerment for everybody. Just like an excel or word.
a group. He can be quite "posh", for example he cancels
people on cs.stackexchange.com, because he claims
the question is not a research question. And then
he finds support for this cancel culture by the charter
of cs.stackexchange.com. So stack exchange sites
are known to implement a form of class racism. There
is a danger that this proof assistant stack exchange site
not only becomes a bitrot exchange, but also
those pieces that are not bitrot do not become accessible
to all, and not everybody can contribute. So it might become
an elite thing like mathoverflow, cs.stackexchange.com, etc..
but logic and set theory for example, should be available
to everyone. Especially via tools they should provide end-user
empowerment for everybody. Just like an excel or word.
Mostowski Collapse
Nov 20, 2021, 9:40:32 AM11/20/21
to
The best would be anyway a new type of Q & A, that supports
a form of literate programming. Literature programming can
be also used in proof assistants. Actually Isabelle/HOL makes
good use of literate programming, their proof archive is just
PDF generated from computer proofs that have also comments
in it, and can be read like a book. But since bitrot exchange
is so lame, they can even not make a syntax highlighter for
the Prolog programming language, proof assistants literature
programming style is definitely not the right place for bitrot
exchange. They are simply way too stupid.
a form of literate programming. Literature programming can
be also used in proof assistants. Actually Isabelle/HOL makes
good use of literate programming, their proof archive is just
PDF generated from computer proofs that have also comments
in it, and can be read like a book. But since bitrot exchange
is so lame, they can even not make a syntax highlighter for
the Prolog programming language, proof assistants literature
programming style is definitely not the right place for bitrot
exchange. They are simply way too stupid.
Mostowski Collapse
Nov 20, 2021, 9:50:16 AM11/20/21
to
A cute new Q & A system would be a system that also provides
compute servers. These servers would do the proofs in the proof
documents. Maybe this can be also done client side, not yet sure.
Usually a theory imports other theories and you got a usual
module network, a client can load all these modules and perform
compute locally. But maybe a hybrid could with some batch
processing could bring some bang. So that the end-user experience
is not interrupted by some heavy processing, instead compute
servers help you invisibly in the background. A new version of
SWISH could maybe do that. The recent discussion about legal
documents and s(CASP) on SWI-Prolog discourse was also interesting.
The scope of the new proof assistant is also quite narrow, and
thinks proof assistants are only used for math and cs, but they
have also uses in philsophical logic, in legal reasoning, etc.. You
find already proof of such use cases in the wild. Just look around.
I already though that bitrot exchange implements a form of
pseudo scientism. The spaw site after site. If there is a site about
camping, a few months later there will be two sites, on for
camping with blue tents and one for camping with red tents.
compute servers. These servers would do the proofs in the proof
documents. Maybe this can be also done client side, not yet sure.
Usually a theory imports other theories and you got a usual
module network, a client can load all these modules and perform
compute locally. But maybe a hybrid could with some batch
processing could bring some bang. So that the end-user experience
is not interrupted by some heavy processing, instead compute
servers help you invisibly in the background. A new version of
SWISH could maybe do that. The recent discussion about legal
documents and s(CASP) on SWI-Prolog discourse was also interesting.
The scope of the new proof assistant is also quite narrow, and
thinks proof assistants are only used for math and cs, but they
have also uses in philsophical logic, in legal reasoning, etc.. You
find already proof of such use cases in the wild. Just look around.
I already though that bitrot exchange implements a form of
pseudo scientism. The spaw site after site. If there is a site about
camping, a few months later there will be two sites, on for
camping with blue tents and one for camping with red tents.
Mostowski Collapse
Nov 20, 2021, 10:04:08 AM11/20/21
to
Don't worry guys, I am not really angry,
I am just doing some brain writing.
> "Holding on to anger is like grasping a hot coal with the
intent of throwing it at someone else; you are the one
who gets burned."
- Buddha
But I guess we can consider bitrot exchange as a scratchpad
that will not last for ethernity. After all singularity will only
happen when we reach this point:
> "Can you imagine that they used to have libraries where
the books didn't even talk to each other?"
- Marvin Minsky, MIT
LoL
I am just doing some brain writing.
> "Holding on to anger is like grasping a hot coal with the
intent of throwing it at someone else; you are the one
who gets burned."
- Buddha
But I guess we can consider bitrot exchange as a scratchpad
that will not last for ethernity. After all singularity will only
happen when we reach this point:
> "Can you imagine that they used to have libraries where
the books didn't even talk to each other?"
- Marvin Minsky, MIT
LoL
Mostowski Collapse
Nov 20, 2021, 1:30:16 PM11/20/21
to
This fits somehow the bitrot exchange topic.
SWI-Prolog wants to measure work in hard money.
Here is my penny (pun) of thought:
Highly qualified work, like contributing to a programming
language implementation without breaking things and writing
documentation, is at least worth 1000 EUR per Day. Which
makes around 100 EUR per Hour. No joke.
Problem is anybody touching a programming language has
to be fit in software architecture. Like juggling with APIs. So
I took a software architect salary from the upper spectrum,
which is around 200’000.- EUR per Year, to account for the
exotic Prolog requirement, and divided it by 200 working
days per Year, which gives me 1000.- per Day.
SWI-Prolog wants to measure work in hard money.
Here is my penny (pun) of thought:
Highly qualified work, like contributing to a programming
language implementation without breaking things and writing
documentation, is at least worth 1000 EUR per Day. Which
makes around 100 EUR per Hour. No joke.
Problem is anybody touching a programming language has
to be fit in software architecture. Like juggling with APIs. So
I took a software architect salary from the upper spectrum,
which is around 200’000.- EUR per Year, to account for the
exotic Prolog requirement, and divided it by 200 working
days per Year, which gives me 1000.- per Day.
Mostowski Collapse
Nov 20, 2021, 1:44:54 PM11/20/21
to
Microsoft would possibly pay at least the double, if they could
get hold of Jan W. himself and if they would mistake Prolog
for Python. Now the position is occupied by Guido R.
get hold of Jan W. himself and if they would mistake Prolog
for Python. Now the position is occupied by Guido R.
Mostowski Collapse
Nov 21, 2021, 1:01:09 PM11/21/21
to
I hope they name it:
qed.stackexchange.com
https://area51.meta.stackexchange.com/a/32603/100686
Although I am not in favor of bitrot exchange in general.
qed.stackexchange.com
https://area51.meta.stackexchange.com/a/32603/100686
Although I am not in favor of bitrot exchange in general.
Mostowski Collapse
Nov 21, 2021, 1:26:09 PM11/21/21
to
Anyway you might need multiple run-ups. For example
an artificial intelligence stackexchange site had a lot
of opposition in the past, and there were multiple
failed run-ups. But today there is:
https://ai.stackexchange.com/
One old argument against it was:
According to the post No Artificial Intelligence in Area 51
the main reason for the failure of the last proposal was
the lack of expert-level questions:
It wasn’t so much the lack of questions that was of concern —
a site can stay in beta as long as it takes — but the conspicuous
lack of expert-level questions. This was also the emerging opinion
amongst the users:
[...]
70-80% of the questions didn’t run much deeper than “When will
we have intelligent computers?” and “What is your favorite AI blog?”
https://area51.meta.stackexchange.com/a/12367/100686
Now everybody is expert in artificial intelligence. You
find even 15 year old youngsters from Kerala, India posting
videos on youtube about Google tensor flow.
LoL
an artificial intelligence stackexchange site had a lot
of opposition in the past, and there were multiple
failed run-ups. But today there is:
https://ai.stackexchange.com/
One old argument against it was:
According to the post No Artificial Intelligence in Area 51
the main reason for the failure of the last proposal was
the lack of expert-level questions:
It wasn’t so much the lack of questions that was of concern —
a site can stay in beta as long as it takes — but the conspicuous
lack of expert-level questions. This was also the emerging opinion
amongst the users:
[...]
70-80% of the questions didn’t run much deeper than “When will
we have intelligent computers?” and “What is your favorite AI blog?”
https://area51.meta.stackexchange.com/a/12367/100686
Now everybody is expert in artificial intelligence. You
find even 15 year old youngsters from Kerala, India posting
videos on youtube about Google tensor flow.
LoL
Mostowski Collapse
Nov 21, 2021, 1:32:48 PM11/21/21
to
BTW: I can assure you "qed" is the best name. Since its
very catchy and the man on the street doesn't know what
it means, similar to "stackoverflow". In the past (2013) there
was also a thinking for the other stackexchange site:
"Don't give it a 'Hollywood' title like 'artificial intelligence'.
Call it "Machine Learning and Intelligent Computation"".
https://area51.meta.stackexchange.com/a/13109/100686
Guess what it is called now?
LoL
very catchy and the man on the street doesn't know what
it means, similar to "stackoverflow". In the past (2013) there
was also a thinking for the other stackexchange site:
"Don't give it a 'Hollywood' title like 'artificial intelligence'.
Call it "Machine Learning and Intelligent Computation"".
https://area51.meta.stackexchange.com/a/13109/100686
Guess what it is called now?
LoL
Dan Christensen
Nov 21, 2021, 4:49:49 PM11/21/21
to
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
Mostowski Collapse
Nov 21, 2021, 9:12:49 PM11/21/21
to
What could be interesting, to combine a stackexchange with
blockchain. For example make a proof a Non-Fungible Token,
and then let the author decided where the proof is
displayed. So a stackexchange would be like a museum,
and the proofs would be unique. But the owner of the proof,
not necessarely the original author, since there can be a
market and trade, can decide whether something is on display?
blockchain. For example make a proof a Non-Fungible Token,
and then let the author decided where the proof is
displayed. So a stackexchange would be like a museum,
and the proofs would be unique. But the owner of the proof,
not necessarely the original author, since there can be a
market and trade, can decide whether something is on display?
Mostowski Collapse
Nov 21, 2021, 9:16:03 PM11/21/21
to
The author of a proof would be free in the choice of his
tools. He could also choose tools that even would assist
him in generating the theorem itself that he would prove.
Whereby the mathematical profession is seen as
hard work and a lot of sweat to found a field and
explore a field, the new profession would be pushing
a button, and new fields would sprout like flowers.
Immortalise Your Valentine in Mathematics - Cavallo, 2011
https://www.prweb.com/releases/theorymine/valentinesdaygeekgifts/prweb5054614.htm
The Theory behind TheoryMine
https://www.researchgate.net/publication/228428155
tools. He could also choose tools that even would assist
him in generating the theorem itself that he would prove.
Whereby the mathematical profession is seen as
hard work and a lot of sweat to found a field and
explore a field, the new profession would be pushing
a button, and new fields would sprout like flowers.
Immortalise Your Valentine in Mathematics - Cavallo, 2011
https://www.prweb.com/releases/theorymine/valentinesdaygeekgifts/prweb5054614.htm
The Theory behind TheoryMine
https://www.researchgate.net/publication/228428155
Mostowski Collapse
Nov 22, 2021, 5:49:32 AM11/22/21
to
Ha Ha, what an ignorant:
QED is a phrase which existed for thousands of years before computers.
This site is specifically about computer proofs, not proofs.
– Kevin Buzzard
Nope. QED is not that old. It became use after the dark ages. So its
only like 500 years old. The abrevation for the greek precursor would
be something like OEΔ.
https://de.wikipedia.org/wiki/Quod_erat_demonstrandum#Herkunft
QED is a phrase which existed for thousands of years before computers.
This site is specifically about computer proofs, not proofs.
– Kevin Buzzard
Nope. QED is not that old. It became use after the dark ages. So its
only like 500 years old. The abrevation for the greek precursor would
be something like OEΔ.
https://de.wikipedia.org/wiki/Quod_erat_demonstrandum#Herkunft
Mostowski Collapse
Nov 22, 2021, 5:51:30 AM11/22/21
to
BTW: This could be also fun:
eureka.stackexchange.com
See also:
en.wikipedia.org/wiki/Eureka_%28word%29#Mathematics
aha.stackexchange.com
See also:
en.wiktionary.org/wiki/aha
eureka.stackexchange.com
See also:
en.wikipedia.org/wiki/Eureka_%28word%29#Mathematics
aha.stackexchange.com
See also:
en.wiktionary.org/wiki/aha
Julio Di Egidio
Nov 22, 2021, 8:26:48 AM11/22/21
to
Die Wendung stammt aus Euklids Lehrbuch Elemente (3. Buch, 4. Kapitel, Theorema XIII) aus dem 3. Jahrhundert v. Chr. und lautet im altgriechischen Original ὅπερ ἔδει δεῖξαι hóper édei deîxai.
You can't even read German... LOL.
*Plonk*
Julio
Mostowski Collapse
Nov 22, 2021, 11:07:24 AM11/22/21
to
ὅπερ ἔδει δεῖξαι
is a different phrase
Mostowski Collapse
Nov 22, 2021, 11:11:59 AM11/22/21
to
The age of a phrase in a certain language, is
determined from when this phrase in a certain
language became use. You can check the same
German wiki, the latin version is very young:
"Die heute verbreitete lateinische Übersetzung prägte
der italienische Humanist Bartolomeo Zamberti, als er
Euklids Elemente übersetzte und 1505 in Venedig drucken ließ."
Or in English:
The Latin translation that is widespread today was shaped by
the Italian humanist Bartolomeo Zamberti when he translated
Euclid's elements and had them printed in Venice in 1505. "
Now do the computation:
2021 - 1505 = 516 = ca. 500 years
determined from when this phrase in a certain
language became use. You can check the same
German wiki, the latin version is very young:
"Die heute verbreitete lateinische Übersetzung prägte
der italienische Humanist Bartolomeo Zamberti, als er
Euklids Elemente übersetzte und 1505 in Venedig drucken ließ."
Or in English:
The Latin translation that is widespread today was shaped by
the Italian humanist Bartolomeo Zamberti when he translated
Euclid's elements and had them printed in Venice in 1505. "
Now do the computation:
2021 - 1505 = 516 = ca. 500 years
Mostowski Collapse
Nov 22, 2021, 11:19:54 AM11/22/21
to
"Although Euclid was known to Cicero, for instance, no
record exists of the text having been translated into Latin
prior to Boethius in the fifth or sixth century.
Although known in Byzantium, the Elements was lost to Western
Europe until about 1120, when the English monk Adelard of Bath
translated it into Latin from an Arabic translation."
https://en.wikipedia.org/wiki/Euclid's_Elements
So there must have been early latin translations, but they didn't
show the famous Q.E.D. ? Or the later date refers to wide
distribution in print?
Mostowski Collapse
Nov 22, 2021, 12:28:16 PM11/22/21
to
Here are some more ideas:
wzbw.stackexchange.com
Abbrevation for "Was zu beweisen war"
cqfd.stackexchange.com
Abbrevation for "ce qu'il fallait démontrer"
cvd.stackexchange.com
Abbrevation for "Come volevasi dimostrare"
LoL
See also:
https://it.wikipedia.org/wiki/Come_volevasi_dimostrare#In_altre_lingue
wzbw.stackexchange.com
Abbrevation for "Was zu beweisen war"
cqfd.stackexchange.com
Abbrevation for "ce qu'il fallait démontrer"
cvd.stackexchange.com
Abbrevation for "Come volevasi dimostrare"
LoL
See also:
https://it.wikipedia.org/wiki/Come_volevasi_dimostrare#In_altre_lingue
Mostowski Collapse
Nov 22, 2021, 12:30:32 PM11/22/21
to
Mostowski Collapse
Nov 22, 2021, 12:33:45 PM11/22/21
to
Julio Di Egidio
Nov 22, 2021, 12:40:26 PM11/22/21
to
On Monday, 22 November 2021 at 17:07:24 UTC+1, Mostowski Collapse wrote:
> ὅπερ ἔδει δεῖξαι
> is a different phrase
You are simply a compulsive case of Dunning-Kruger. The very next sentence of the very same article says "Die heute verbreitete lateinische Übersetzung prägte der italienische Humanist Bartolomeo Zamberti, als er Euklids Elemente übersetzte und 1505 in Venedig drucken ließ", which is about how Euclid's expression became the "QED" we all use today.
> ὅπερ ἔδει δεῖξαι
> is a different phrase
Try and get a grip...
(EOD.)
Julio
Mostowski Collapse
Nov 22, 2021, 1:08:29 PM11/22/21
to
Yes that is what we I initially wrote:
Mostowski Collapse schrieb am Montag, 22. November 2021 um 11:49:32 UTC+1:
> Nope. QED is not that old. It became use after the dark ages. So its
> only like **500 years old**. The abrevation for the greek precursor would
https://groups.google.com/g/sci.logic/c/qFoJgqZV5-g/m/1OhepxoBBAAJ
Cant you subtract 2021 (the year we have now)
and the year 1505 (given in Wikipedia).
Whats wrong with you?
Mostowski Collapse schrieb am Montag, 22. November 2021 um 11:49:32 UTC+1:
> Nope. QED is not that old. It became use after the dark ages. So its
https://groups.google.com/g/sci.logic/c/qFoJgqZV5-g/m/1OhepxoBBAAJ
Cant you subtract 2021 (the year we have now)
and the year 1505 (given in Wikipedia).
Whats wrong with you?
Julio Di Egidio
Nov 22, 2021, 1:10:51 PM11/22/21
to
On Monday, 22 November 2021 at 19:08:29 UTC+1, Mostowski Collapse wrote:
> Yes that is what we I initially wrote:
What you wrote initially is "Ha Ha, what an ignorant".
> Yes that is what we I initially wrote:
Try and get a grip...
Julio
Mostowski Collapse
Nov 22, 2021, 1:13:41 PM11/22/21
to
Somebody needs to slap Culio into the face, so that
he wakes up, he is asleep in the front of his computer
screen, and doesn't see what is written:
als er Euklids Elemente übersetzte und **1505 in Venedig** drucken ließ
1505
in
Venedig
:::'##:::'########:::'#####:::'########:
:'####::: ##.....:::'##.. ##:: ##.....::
:.. ##::: ##:::::::'##:::: ##: ##:::::::
::: ##::: #######:: ##:::: ##: #######::
::: ##:::...... ##: ##:::: ##:...... ##:
::: ##:::'##::: ##:. ##:: ##::'##::: ##:
:'######:. ######:::. #####:::. ######::
:......:::......:::::.....:::::......:::
he wakes up, he is asleep in the front of his computer
screen, and doesn't see what is written:
als er Euklids Elemente übersetzte und **1505 in Venedig** drucken ließ
1505
in
Venedig
:::'##:::'########:::'#####:::'########:
:'####::: ##.....:::'##.. ##:: ##.....::
:.. ##::: ##:::::::'##:::: ##: ##:::::::
::: ##::: #######:: ##:::: ##: #######::
::: ##:::...... ##: ##:::: ##:...... ##:
::: ##:::'##::: ##:. ##:: ##::'##::: ##:
:'######:. ######:::. #####:::. ######::
:......:::......:::::.....:::::......:::
Mostowski Collapse
Nov 28, 2021, 10:22:14 AM11/28/21
to
This shows me that functional programming is on the decline:
Google Trends: Logic vs Functional Programming - From 2004 to 2021
https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
I wonder whether this will have an impact on proof assistants.
Some of them have clearly a functional programming inclining.
Google Trends: Logic vs Functional Programming - From 2004 to 2021
https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
I wonder whether this will have an impact on proof assistants.
Some of them have clearly a functional programming inclining.
Mostowski Collapse
Nov 28, 2021, 10:28:28 AM11/28/21
to
This is also an interesting article, mentioning a new
trend such as "Multiparadigm languages":
Where Programming, Ops, AI, and the Cloud are Headed in 20
https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
We just observed that Python 3.10 introduced a new
pattern matching construct. Now there is a proposal
for Java JDK 17 followup for some pattern matching
like switch statement. I guess there is an unspoken law:
"Every programming language over the long
run will evolve into some Prolog variant"
Well this is too harsh, maybe this pattern matching only
mimicks Haskell single sided unification and not Prolog
unification. But what if people get fed up
with single sided unification?
LoL
trend such as "Multiparadigm languages":
Where Programming, Ops, AI, and the Cloud are Headed in 20
https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
We just observed that Python 3.10 introduced a new
pattern matching construct. Now there is a proposal
for Java JDK 17 followup for some pattern matching
like switch statement. I guess there is an unspoken law:
"Every programming language over the long
run will evolve into some Prolog variant"
Well this is too harsh, maybe this pattern matching only
mimicks Haskell single sided unification and not Prolog
unification. But what if people get fed up
with single sided unification?
LoL
Mostowski Collapse
Nov 28, 2021, 2:30:46 PM11/28/21
to
Maybe the assumption that programming language further
evolve is wrong, they could also devolve to assembler again?
Awaken In 2505, Humans Devolve
https://www.youtube.com/watch?v=mnLxc954ipo
At least this would truely help to have full control of
the performance and memory allocation of your code.
LMAO!
evolve is wrong, they could also devolve to assembler again?
Awaken In 2505, Humans Devolve
https://www.youtube.com/watch?v=mnLxc954ipo
At least this would truely help to have full control of
the performance and memory allocation of your code.
LMAO!
Mostowski Collapse
Nov 30, 2021, 8:33:50 AM11/30/21
to
A glimpse what might come in the future, even solely
in the client, no need for server roundtrips, and very
nice rendering of formulas:
Automated Propositional Sequent Proofs
in Your Browser with Tau Prolog
Feb 7, 2021 • Philip Zucker
https://www.philipzucker.com/javascript-automated-proving/
If bitrot stackexchanges adopts something from MSE
it could reach such rendering. But SO can even not
render Prolog code correctly.
in the client, no need for server roundtrips, and very
nice rendering of formulas:
Automated Propositional Sequent Proofs
in Your Browser with Tau Prolog
Feb 7, 2021 • Philip Zucker
https://www.philipzucker.com/javascript-automated-proving/
If bitrot stackexchanges adopts something from MSE
it could reach such rendering. But SO can even not
render Prolog code correctly.
Daniel Pehoushek
Nov 30, 2021, 9:03:46 AM11/30/21
to
a competent question be presented ?
already with a competent answer.
Then the absurd dependence on universal ignorance
to provide me with my answer is removed completely.
cs theory stack ez change is so full of shit they do not let me post.
bob does three trillion inferences per day
monotone reason is linearly decidable
P=NP for small but not large numbers
hashfind is the optimal pattern recognition core of the systems
+abcd vision is n log base four of n vision on n bits
#P=#Q : number of questions equals number of facts
daniel gres2380
Mostowski Collapse
Nov 30, 2021, 9:09:35 AM11/30/21
to
The devolution could be also a form of evolution. I recently saw
a book about ARM assembly which had a garbage collection
section. In 2018 ARM started supporting pointer tagging.
See also:
ARM Memory Tagging Extension
Kosty Serbryany - 2019
https://www.usenix.org/system/files/login/articles/login_summer19_03_serebryany.pdf
C–: a portable assembly language that supports garbage collection
Simon Peyton Jones - 1999
https://www.cs.tufts.edu/~nr/pubs/c–gc.pdf
Basically what was once conceived as a Java Chip seems to
happen right now. You can also view it as LISP on a Chip I guess,
remove the object oriented obsession, and focus on safety.
a book about ARM assembly which had a garbage collection
section. In 2018 ARM started supporting pointer tagging.
See also:
ARM Memory Tagging Extension
Kosty Serbryany - 2019
https://www.usenix.org/system/files/login/articles/login_summer19_03_serebryany.pdf
C–: a portable assembly language that supports garbage collection
Simon Peyton Jones - 1999
https://www.cs.tufts.edu/~nr/pubs/c–gc.pdf
Basically what was once conceived as a Java Chip seems to
happen right now. You can also view it as LISP on a Chip I guess,
remove the object oriented obsession, and focus on safety.
Daniel Pehoushek
Nov 30, 2021, 9:14:11 AM11/30/21
to
at three trillion inferences per day
cs theory stack ez change is so full of shit they do not let me post.
I much prefer for a trivial education page that
a competent question be presented ?
already with a competent answer.
Then the absurd dependence on universal ignorance
to provide me with my answer is removed completely.
monotone reason is linearly decidable
P=NP for small but not large numbers
hashfind is the optimal pattern recognition core of the systems
+abcd vision is n log base four of n vision on n bits
#P=#Q : number of questions equals number of facts
daniel 2380 of 2400 in 1983
P=NP for small but not large numbers
hashfind is the optimal pattern recognition core of the systems
+abcd vision is n log base four of n vision on n bits
#P=#Q : number of questions equals number of facts
Daniel Pehoushek
Nov 30, 2021, 9:23:14 AM11/30/21
to
when disjoint logical components of any sub formula are detected
bob computes the bignum answer on each component in a series
multiplies (including zero) into the whole answer and then
places the bignum space used for the previous component
onto a bigstack of logn bignum data structures.
memory allocation for reason by bob is linear which is similar to human
daniel
Mostowski Collapse
Dec 1, 2021, 7:52:53 PM12/1/21
to
Generating theorems itself has now a name:
CAH: Computer assisted seeing of patterns aka halucinations?
"More than a century ago, Srinivasa Ramanujan shocked
the mathematical world with his extraordinary ability to
see remarkable patterns in numbers that no one else
could see. The self-taught mathematician from India
described his insights as deeply intuitive and spiritual,
and patterns often came to him in vivid dreams."
"The use of learning techniques and AI systems holds
great promise for the identification and discovery of
patterns in mathematics. Even if certain kinds of patterns
continue to elude modern ML, we hope our Nature paper
can inspire other researchers to consider the potential
for AI as a useful tool in pure maths."
https://deepmind.com/blog/article/exploring-the-beauty-of-pure-mathematics-in-novel-ways
LoL
CAH: Computer assisted seeing of patterns aka halucinations?
"More than a century ago, Srinivasa Ramanujan shocked
the mathematical world with his extraordinary ability to
see remarkable patterns in numbers that no one else
could see. The self-taught mathematician from India
described his insights as deeply intuitive and spiritual,
and patterns often came to him in vivid dreams."
"The use of learning techniques and AI systems holds
great promise for the identification and discovery of
patterns in mathematics. Even if certain kinds of patterns
continue to elude modern ML, we hope our Nature paper
can inspire other researchers to consider the potential
for AI as a useful tool in pure maths."
https://deepmind.com/blog/article/exploring-the-beauty-of-pure-mathematics-in-novel-ways
LoL
Mostowski Collapse
Dec 4, 2021, 10:27:01 AM12/4/21
to
Works also inside SWISH, try this SWISH Prolog text:
https://swish.swi-prolog.org/p/phil_zucker.pl
Only SWISH shows the result with writeq/1 and not with write/1:
Proof = rimpl([]>[('A' & 'B' => 'A')], land([('A' & 'B')]>['A'],
ax(['A', 'B']>['A'], 'A')))
Now somebody add a MathJax SWISH renderer?
https://swish.swi-prolog.org/p/phil_zucker.pl
Only SWISH shows the result with writeq/1 and not with write/1:
Proof = rimpl([]>[('A' & 'B' => 'A')], land([('A' & 'B')]>['A'],
ax(['A', 'B']>['A'], 'A')))
Now somebody add a MathJax SWISH renderer?
Mostowski Collapse
Dec 5, 2021, 11:59:25 AM12/5/21
to
Would be really interesting to see how fast SWISH round trip would
be for other logics than only classical propositonal logic, as in Phil Zuckers
prove0/2 above. Also nice MathJax dressing inside SWISH would be cool.
This trivia takes quite some time, but requires FOL with equality:
∀a∀b∀c((Fab ∧ Fac) → b=c) ∧
(∀a(¬a=z ↔ ∃bFab) ∧
∀a∀b(Fab ↔ m(a,b)=o))
entails ∀a(¬a=z → ∃b(Fab ∧ m(a,b)=o)).
https://www.umsu.de/trees
But maybe the time is consumed because the online tool by Wolfgang
Schwarz does two things at once, trying to find a proof and trying to find
a counter model? Not sure.
Also ∀a∀b∀c((Fab ∧ Fac) → b=c) is a decoy, not needed in the proof,
which slows down the proof search I guess.
be for other logics than only classical propositonal logic, as in Phil Zuckers
prove0/2 above. Also nice MathJax dressing inside SWISH would be cool.
This trivia takes quite some time, but requires FOL with equality:
∀a∀b∀c((Fab ∧ Fac) → b=c) ∧
(∀a(¬a=z ↔ ∃bFab) ∧
∀a∀b(Fab ↔ m(a,b)=o))
entails ∀a(¬a=z → ∃b(Fab ∧ m(a,b)=o)).
https://www.umsu.de/trees
But maybe the time is consumed because the online tool by Wolfgang
Schwarz does two things at once, trying to find a proof and trying to find
a counter model? Not sure.
Also ∀a∀b∀c((Fab ∧ Fac) → b=c) is a decoy, not needed in the proof,
which slows down the proof search I guess.
Mostowski Collapse
Dec 28, 2021, 1:24:46 PM12/28/21
to
Interesting call:
"For example, have a look at the Coq standard libarary or
the user contributions, these are formalizations of
mathematics in type theory. And this stuff is written mostly
by computer scientists. If mathematicians moved onto
the proof-assistant bandwagon, there would be much more."
https://mathoverflow.net/a/133599
Maybe they would join the bandwagon if there were
less typos? Whats a "libarary"? Is it library? Or libarray?
LoL
"For example, have a look at the Coq standard libarary or
the user contributions, these are formalizations of
mathematics in type theory. And this stuff is written mostly
by computer scientists. If mathematicians moved onto
the proof-assistant bandwagon, there would be much more."
https://mathoverflow.net/a/133599
Maybe they would join the bandwagon if there were
less typos? Whats a "libarary"? Is it library? Or libarray?
LoL
Mostowski Collapse
Dec 29, 2021, 5:45:49 PM12/29/21
to
Small bug in the LK code:
There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
https://www.philipzucker.com/javascript-automated-proving/
Its not complete for FOL matrices, try this:
prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
Failed To Prove.
Now remove the cut in the axiom rule:
prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
X = s
There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
https://www.philipzucker.com/javascript-automated-proving/
Its not complete for FOL matrices, try this:
prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
Failed To Prove.
Now remove the cut in the axiom rule:
prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
X = s
Mostowski Collapse
Dec 30, 2021, 3:55:43 AM12/30/21
to
To handle FOL matrices, unify_with_occurs_check/2 might
also come into play. Whats a short example and short
explanation about things that can go wrong?
Mostowski Collapse schrieb:
also come into play. Whats a short example and short
explanation about things that can go wrong?
Mostowski Collapse schrieb:
Mostowski Collapse
Dec 30, 2021, 4:07:19 AM12/30/21
to
Oh, this is very nice!
∃x∃y(Pyy → Pxf(x)) is invalid.
https://www.umsu.de/trees/#~7x~7y%28Pyy~5Pxf%28x%29%29
Countermodel:
Domain: { 0, 1 }
f: { (0,1), (1,0) }
P: { (0,0), (1,1) }
∃x∃y(Pyy → Pxf(x)) is invalid.
https://www.umsu.de/trees/#~7x~7y%28Pyy~5Pxf%28x%29%29
Countermodel:
Domain: { 0, 1 }
f: { (0,1), (1,0) }
P: { (0,0), (1,1) }
Serg io
Dec 30, 2021, 10:41:23 AM12/30/21
to
the search for funding never seizes
Mostowski Collapse
Jan 2, 2022, 6:30:10 PM1/2/22
to
Oki Doki, full first order logic can be also rendered now:
Leibniz’s Dream in Dogelog Player
https://twitter.com/dogelogch/status/1477779371628933121
Leibniz’s Dream in Dogelog Player
https://www.facebook.com/groups/dogelog
Leibniz’s Dream in Dogelog Player
https://twitter.com/dogelogch/status/1477779371628933121
Leibniz’s Dream in Dogelog Player
https://www.facebook.com/groups/dogelog
Mostowski Collapse
Jan 16, 2022, 7:27:48 AM1/16/22
to
Now having fun with an output switch, can do:
?- parse('∀x ∃y f(x) = y', F).
F = !(:([_0 = x], ?(:([_1 = y], f(_0) = _1)))).
?- unparse(!(:([A = x], ?(:([B = y], f(A) = B)))), unicode, T).
T = '∀x ∃y f(x) = y'.
?- unparse(!(:([A = x], ?(:([B = y], f(A) = B)))), latex, T).
T = '\\forall x\\, \\exists y\\, \\mathup{f}(x) = y'.
The LaTeX DCG result can be used inside a browser via MathJax.
But with the novel operator type fzy, that is used under the hood,
I am also solving another problem, not only LaTeX output.
The other problem that is also solved is dealing with input and output
of formulas that contain quantifiers. The library is now called
Formula Interlingua Library (FIL).
See also:
Formula Interlingua from Prolog Operator Syntax
https://twitter.com/dogelogch/status/1482536744872521732
Formula Interlingua from Prolog Operator Syntax
https://www.facebook.com/groups/dogelog
?- parse('∀x ∃y f(x) = y', F).
F = !(:([_0 = x], ?(:([_1 = y], f(_0) = _1)))).
?- unparse(!(:([A = x], ?(:([B = y], f(A) = B)))), unicode, T).
T = '∀x ∃y f(x) = y'.
?- unparse(!(:([A = x], ?(:([B = y], f(A) = B)))), latex, T).
T = '\\forall x\\, \\exists y\\, \\mathup{f}(x) = y'.
The LaTeX DCG result can be used inside a browser via MathJax.
But with the novel operator type fzy, that is used under the hood,
I am also solving another problem, not only LaTeX output.
The other problem that is also solved is dealing with input and output
of formulas that contain quantifiers. The library is now called
Formula Interlingua Library (FIL).
See also:
Formula Interlingua from Prolog Operator Syntax
https://twitter.com/dogelogch/status/1482536744872521732
Formula Interlingua from Prolog Operator Syntax
https://www.facebook.com/groups/dogelog
Mostowski Collapse
Jan 16, 2022, 7:31:33 AM1/16/22
to
Adding MathJax to your web site is very simple,
bypassing the now outdated and not widely
supported MathML. MathJax notes the following
problems with MathML:
> CommonHTML and not MathML is MathJax’s primary output
> mode since MathJax version 2.6. Its major advantage is its
> quality, consistency, and the fact that its output is independent
> of the browser, operating system, and user environment.
> HTML Support — MathJax 3.2 documentation
> https://docs.mathjax.org/en/latest/output/html.html
This worked for me:
- Step 1: Load the MathJax library. Load the CommonHTML
output processor (chtml), that renders your mathematics
using HTML with CSS styling:
<script src="http://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js"
id="MathJax-script" async=""> </script>
- Step 2: Make the MathJax library load some stuff by itself.
This is a little cludge, not sure what would be the official
approach here, this loads bussproof:
<p>\begin{prooftree} \end{prooftree}</p>
- Step 3: Notify MathJax library if you have DOM changes. Not
needed after browser page load, only for user interaction. Do
this JavaScript when you are finished doing updates:
MathJax.typeset();
bypassing the now outdated and not widely
supported MathML. MathJax notes the following
problems with MathML:
> CommonHTML and not MathML is MathJax’s primary output
> mode since MathJax version 2.6. Its major advantage is its
> quality, consistency, and the fact that its output is independent
> of the browser, operating system, and user environment.
> HTML Support — MathJax 3.2 documentation
> https://docs.mathjax.org/en/latest/output/html.html
This worked for me:
- Step 1: Load the MathJax library. Load the CommonHTML
output processor (chtml), that renders your mathematics
using HTML with CSS styling:
<script src="http://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js"
id="MathJax-script" async=""> </script>
- Step 2: Make the MathJax library load some stuff by itself.
This is a little cludge, not sure what would be the official
approach here, this loads bussproof:
<p>\begin{prooftree} \end{prooftree}</p>
- Step 3: Notify MathJax library if you have DOM changes. Not
needed after browser page load, only for user interaction. Do
this JavaScript when you are finished doing updates:
MathJax.typeset();
Mostowski Collapse
Jan 16, 2022, 8:59:21 PM1/16/22
to
Some papers show calculi with two substitution rules
where the equation appears as ~(s=t) and flipped
as ~(t=s). Strange in our take we dont need this,
only flipped polarity of atomic formulas, this
is provable with a=b in it:
1. a = b ∧ p(a) ⇒ p(b)
2. p(b) (T⇒2 1)
3. ¬(a = b ∧ p(a)) (T⇒1 1)
4. ¬p(a) (F∧2 3)
5. ¬a = b (F∧1 3)
6. ¬p(b) (F= 5, 4)
✓ (ax 6, 2)
And now with flipped b=a, it works as well:
1. b = a ∧ p(a) ⇒ p(b)
2. p(b) (T⇒2 1)
3. ¬(b = a ∧ p(a)) (T⇒1 1)
4. ¬p(a) (F∧2 3)
5. ¬b = a (F∧1 3)
6. p(a) (F= 5, 2)
✓ (ax 4, 6)
See also:
First-Order Equality for Maslovs Method
https://twitter.com/dogelogch/status/1482885333486379015
First-Order Equality for Maslovs Method
https://www.facebook.com/groups/dogelog
where the equation appears as ~(s=t) and flipped
as ~(t=s). Strange in our take we dont need this,
only flipped polarity of atomic formulas, this
is provable with a=b in it:
1. a = b ∧ p(a) ⇒ p(b)
2. p(b) (T⇒2 1)
3. ¬(a = b ∧ p(a)) (T⇒1 1)
4. ¬p(a) (F∧2 3)
5. ¬a = b (F∧1 3)
6. ¬p(b) (F= 5, 4)
✓ (ax 6, 2)
And now with flipped b=a, it works as well:
1. b = a ∧ p(a) ⇒ p(b)
2. p(b) (T⇒2 1)
3. ¬(b = a ∧ p(a)) (T⇒1 1)
4. ¬p(a) (F∧2 3)
5. ¬b = a (F∧1 3)
6. p(a) (F= 5, 2)
✓ (ax 4, 6)
See also:
First-Order Equality for Maslovs Method
https://twitter.com/dogelogch/status/1482885333486379015
First-Order Equality for Maslovs Method
https://www.facebook.com/groups/dogelog
Mostowski Collapse
Jan 18, 2022, 10:58:09 AM1/18/22
to
I did the barber paradox always wrong!
The biconditional makes it so much easier.
1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
5. ¬¬s(a, a) (F∧2 4)
6. ¬s(a, a) (F∧1 4)
7. s(a, a) (F¬ 5)
✓ (ax 6, 7)
4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
5. ¬s(a, a) (T∨2 4)
6. s(a, a) (T∨1 4)
✓ (ax 5, 6)
See also:
Biconditional Support for Maslovs Method
https://twitter.com/dogelogch/status/1483455561031106563
Biconditional Support for Maslovs Method
https://www.facebook.com/groups/dogelog
The biconditional makes it so much easier.
1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
5. ¬¬s(a, a) (F∧2 4)
6. ¬s(a, a) (F∧1 4)
7. s(a, a) (F¬ 5)
✓ (ax 6, 7)
4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
5. ¬s(a, a) (T∨2 4)
6. s(a, a) (T∨1 4)
✓ (ax 5, 6)
See also:
Biconditional Support for Maslovs Method
https://twitter.com/dogelogch/status/1483455561031106563
Biconditional Support for Maslovs Method
https://www.facebook.com/groups/dogelog
Mostowski Collapse
Jan 20, 2022, 9:04:14 AM1/20/22
to
Its a pitty that there is no simple leanTap=, i.e. leanTap= with
equality. My take is only a few lines, splitting (subst) into (subst1)
and (subst2) and can run in the browser.
On the other hand I read:
The completion-based method for mixed E-unification we
have described, has been implemented as part of the
tableau-based theorem prover 3TAP [3]. The implementation
consists of about 2500 lines of code, written in Quintus Prolog.
Besides the possibility to prove theorems from predicate logic
with equality, the E-unification module can be used “stand alone”
to solve simultaneous mixed E-unification problems.
https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf
I don’t know how to run 2500 lines of code in the browser.
And I don’t need some first order equality that would even
deploy some term order, as is popular in certain term
rewriting and Knuth Bendix. One interesting test case is this
one, that works in the browser:
?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\
f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
% Wall 60 ms, gc 0 ms, 1171000 lips
Thanks to McCarthys trick its quite fast. On monday it still took
me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz
tool can do the same, but interestingly he gets a longer proof with
more (subst) applications. See also this ticket:
Does the tree tool search shortest proofs? #11
https://github.com/wo/tpg/issues/11
equality. My take is only a few lines, splitting (subst) into (subst1)
and (subst2) and can run in the browser.
On the other hand I read:
The completion-based method for mixed E-unification we
have described, has been implemented as part of the
tableau-based theorem prover 3TAP [3]. The implementation
consists of about 2500 lines of code, written in Quintus Prolog.
Besides the possibility to prove theorems from predicate logic
with equality, the E-unification module can be used “stand alone”
to solve simultaneous mixed E-unification problems.
https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf
I don’t know how to run 2500 lines of code in the browser.
And I don’t need some first order equality that would even
deploy some term order, as is popular in certain term
rewriting and Knuth Bendix. One interesting test case is this
one, that works in the browser:
?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\
f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
% Wall 60 ms, gc 0 ms, 1171000 lips
Thanks to McCarthys trick its quite fast. On monday it still took
me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz
tool can do the same, but interestingly he gets a longer proof with
more (subst) applications. See also this ticket:
Does the tree tool search shortest proofs? #11
https://github.com/wo/tpg/issues/11
Mostowski Collapse
Jan 20, 2022, 9:06:57 AM1/20/22
to
See also my blog post on medium.com:
McCarthys Trick for First Order Equality
https://twitter.com/dogelogch/status/1484032442717585409
McCarthys Trick for First Order Equality
https://www.facebook.com/groups/dogelog
McCarthys Trick for First Order Equality
https://twitter.com/dogelogch/status/1484032442717585409
McCarthys Trick for First Order Equality
https://www.facebook.com/groups/dogelog
Mostowski Collapse
Jan 22, 2022, 7:29:26 PM1/22/22
to
Here is a poket McCarthy for propositional logic only.
It can also do Joseph Vidal-Rossets antisequent (asq):
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
prove(G>[~A,B|D],P).
prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
prove(G>[A,B|D],P).
/* double negation */
prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
prove(G>[A|D],P).
prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
prove(G>[~A,~B|D],P).
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
prove(G>[~A,~B|D],P1),
prove(G>[A,B|D],P2).
prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[~B|D],P2).
prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[B|D],P2).
prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
prove(G>[~A|D],P1),
prove(G>[~B|D],P2).
prove(G>[A|D], ax(G>[A|D], A)):-
member(B,G), A==B, !.
/* next */
prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
prove([A|G]>D,P).
prove(G>[A|D], lneg(G>[A|D], P)) :- !,
prove([~A|G]>D,P).
prove(G>[], asq(G>[], asq)).
provable(F,P):-
prove([]>[F],P).
member(E, [E|_]).
member(E, [_|Xs]) :-
member(E, Xs).
It can also do Joseph Vidal-Rossets antisequent (asq):
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
prove(G>[~A,B|D],P).
prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
prove(G>[A,B|D],P).
/* double negation */
prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
prove(G>[A|D],P).
prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
prove(G>[~A,~B|D],P).
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
prove(G>[~A,~B|D],P1),
prove(G>[A,B|D],P2).
prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[~B|D],P2).
prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[B|D],P2).
prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
prove(G>[~A|D],P1),
prove(G>[~B|D],P2).
prove(G>[A|D], ax(G>[A|D], A)):-
member(B,G), A==B, !.
/* next */
prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
prove([A|G]>D,P).
prove(G>[A|D], lneg(G>[A|D], P)) :- !,
prove([~A|G]>D,P).
prove(G>[], asq(G>[], asq)).
provable(F,P):-
prove([]>[F],P).
member(E, [E|_]).
member(E, [_|Xs]) :-
member(E, Xs).
Mostowski Collapse
Jan 22, 2022, 7:30:41 PM1/22/22
to
Why does Jens Otten automatic reordering preprocessing
give some bang? Now I get for Pelletier problem 71:
/* Joseph Vidal-Rossets LeanSeq, from his web site */
?- test.
% 54,202,362 inferences, 4.969 CPU in 5.017 seconds
(99% CPU, 10908954 Lips)
true.
https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html
/* My McCarthy */
?- test2.
% 8,814,592 inferences, 1.099 CPU in 1.123 seconds
(98% CPU, 8019776 Lips)
true.
I think this is because rbicond is more symmetric,
in my new McCarthy it is now:
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
On the other hand Joseph Vidal-Rossets LeanSeq
has the following rbicond rule:
prove(G>D, rbicond(G>D,P1,P2)):-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],P1),
prove([B|G]>[A|D1], P2).
But this works only for Pelletier problem 71.
The rule is still quite static, and doesn't
do any reordering.
give some bang? Now I get for Pelletier problem 71:
/* Joseph Vidal-Rossets LeanSeq, from his web site */
?- test.
% 54,202,362 inferences, 4.969 CPU in 5.017 seconds
(99% CPU, 10908954 Lips)
true.
https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html
/* My McCarthy */
?- test2.
% 8,814,592 inferences, 1.099 CPU in 1.123 seconds
(98% CPU, 8019776 Lips)
true.
I think this is because rbicond is more symmetric,
in my new McCarthy it is now:
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
has the following rbicond rule:
prove(G>D, rbicond(G>D,P1,P2)):-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],P1),
prove([B|G]>[A|D1], P2).
But this works only for Pelletier problem 71.
The rule is still quite static, and doesn't
do any reordering.
Mostowski Collapse
Jan 22, 2022, 7:31:39 PM1/22/22
to
There is a bug in nff_pure.pl by Jens Otten. This here:
Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,
Should read, so that it runs in a wider variety of Prolog systems:
Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,
And we can now try Pelletier problem 71, and it doesn’t work:
% 88,652,639 inferences, 13.734 CPU in 13.999 seconds
(98% CPU, 6454800 Lips)
ERROR: Stack limit (1.0Gb) exceeded
Strange...
Mostowski Collapse schrieb:
Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,
Should read, so that it runs in a wider variety of Prolog systems:
Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,
And we can now try Pelletier problem 71, and it doesn’t work:
% 88,652,639 inferences, 13.734 CPU in 13.999 seconds
(98% CPU, 6454800 Lips)
ERROR: Stack limit (1.0Gb) exceeded
Strange...
Mostowski Collapse schrieb:
Mostowski Collapse
Jan 23, 2022, 10:56:00 AM1/23/22
to
If I paste my poket McCarthy into Joseph Vidal-Rossets web
page, I can reproduce the example from page 7 of this paper:
leanTAP Revisited
Melvin Fitting - March 13, 1997
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf
Simply use this here:
?- provable(((~p & q) | p), Proof).
The red color shows where the proof tree ends in Γ |- .
Joseph Vidal-Rosset could make a fork of his website,
that provides poket McCarthy directly for experimentation,
also using better proof tree lables. My own web site
does not yet show some red color. Thats a little too
early. First need to get my head around model finding
from tableaux for the non-propositional case...
page, I can reproduce the example from page 7 of this paper:
leanTAP Revisited
Melvin Fitting - March 13, 1997
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf
Simply use this here:
?- provable(((~p & q) | p), Proof).
The red color shows where the proof tree ends in Γ |- .
Joseph Vidal-Rosset could make a fork of his website,
that provides poket McCarthy directly for experimentation,
also using better proof tree lables. My own web site
does not yet show some red color. Thats a little too
early. First need to get my head around model finding
from tableaux for the non-propositional case...
Mostowski Collapse
Jan 23, 2022, 4:03:32 PM1/23/22
to
This one is much shorter, 6 pages code by Triska, 2015:
Prolog implementation of the Knuth-Bendix completion procedure
https://www.metalevel.at/trs/
But is it lean? Something shorter maybe?
Prolog implementation of the Knuth-Bendix completion procedure
https://www.metalevel.at/trs/
But is it lean? Something shorter maybe?
Mostowski Collapse
Jan 24, 2022, 5:37:44 AM1/24/22
to
Melvin Fitting uses the anti-sequents in a semantic completeness
argument. This then explains how validity proving is relatated to SAT
solving. Actually to be precise, validity is UNSAT. For randomized
algorithms there are complexity results for (SAT, ε-UNSAT). But these
results only appeared in recent years.
argument. This then explains how validity proving is relatated to SAT
solving. Actually to be precise, validity is UNSAT. For randomized
algorithms there are complexity results for (SAT, ε-UNSAT). But these
results only appeared in recent years.
Mostowski Collapse
Jan 30, 2022, 3:11:51 PM1/30/22
to
Today a little show of what can go wrong: Question
was why does Jens Otten leanseq_v5.pl use this:
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
And not this:
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
copy_term((X:A,FV),(f_sk(J):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
The offending test case is this here:
∀y∃xFxy → ∃z∀tFzt is invalid.
Countermodel:
Domain: { 0, 1 }
F: { (0,0), (1,1) }
https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt
was why does Jens Otten leanseq_v5.pl use this:
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
And not this:
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
copy_term((X:A,FV),(f_sk(J):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
The offending test case is this here:
∀y∃xFxy → ∃z∀tFzt is invalid.
Countermodel:
Domain: { 0, 1 }
F: { (0,0), (1,1) }
https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt
Mostowski Collapse
Jan 30, 2022, 3:14:21 PM1/30/22
to
I guess there is some literature that explains everything. On the
other hand some Prolog experimentation could maybe help
increase intuition. leanseq_v5.pl first, and I get, limiting the
depth to 10, it already takes quite some time with 10 in this
automated prover which doesn’t have much optimizations:
% leanseq_v5.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
iteration 3
iteration 4
iteration 5
iteration 6
iteration 7
iteration 8
iteration 9
iteration 10
false.
Now the faulty leanseq_v5f.pl, where the Skolem function
is replaced by only a Skolem constant:
% leanseq_v5f.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
true
other hand some Prolog experimentation could maybe help
increase intuition. leanseq_v5.pl first, and I get, limiting the
depth to 10, it already takes quite some time with 10 in this
automated prover which doesn’t have much optimizations:
% leanseq_v5.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
iteration 3
iteration 4
iteration 5
iteration 6
iteration 7
iteration 8
iteration 9
iteration 10
false.
Now the faulty leanseq_v5f.pl, where the Skolem function
is replaced by only a Skolem constant:
% leanseq_v5f.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
true
Mostowski Collapse
Jan 30, 2022, 3:20:22 PM1/30/22
to
Anyway, because nobody has time to wait for ZDD provide a model
finder or to wait that theorem prover has finished its infinitely many
iterations, to show that a formula isn’t provable.
I started publishing a counter model finder for my new Dogelog player.
This is a first beginning, more posts will follow.
Boole’s Method from 1847 in Dogelog Player
https://twitter.com/dogelogch/status/1487845636993134596
Boole’s Method from 1847 in Dogelog Player
https://www.facebook.com/groups/dogelog
finder or to wait that theorem prover has finished its infinitely many
iterations, to show that a formula isn’t provable.
I started publishing a counter model finder for my new Dogelog player.
This is a first beginning, more posts will follow.
Boole’s Method from 1847 in Dogelog Player
https://twitter.com/dogelogch/status/1487845636993134596
Boole’s Method from 1847 in Dogelog Player
https://www.facebook.com/groups/dogelog
Mostowski Collapse
Feb 8, 2022, 6:28:33 AM2/8/22
to
You can run leanTap in Dogelog player in the browser. For the
simple problems among Pelletier 17-46 I get the following
results (100 iterations, browser was Chrome no async/await):
System Time
Tau Prolog 323’000
Dogelog Player 2’441
Formerly Jekejeke 811
SWI 299
Will post a link to a fork later. I want to compare different normal
forms, but still struggling with optimal way to compute prenex and
mini-scope. Too large design space, so slow progress.
The simple problems are:
17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44
simple problems among Pelletier 17-46 I get the following
results (100 iterations, browser was Chrome no async/await):
System Time
Tau Prolog 323’000
Dogelog Player 2’441
Formerly Jekejeke 811
SWI 299
Will post a link to a fork later. I want to compare different normal
forms, but still struggling with optimal way to compute prenex and
mini-scope. Too large design space, so slow progress.
The simple problems are:
17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44
Mostowski Collapse
Feb 10, 2022, 11:28:32 AM2/10/22
to
Now I have obtained a new result, leanTap is not really needed,
leanSeq could also do? I was using negation normal form with leanSeq,
and now leanSeq is also extremly fast. Maybe because of some indexing?
I used a leanSeq variant that saturates the literals before it tries the quantifier.
When I compare the two, there is not anymore much difference between leanSeq
and leanTap. Only the new leanSeq would allow easy proof extraction:
/* leanTap */
?- time((between(1,100,_), test(time), fail; true)).
% 3,011,100 inferences, 0.203 CPU in 0.206 seconds (99% CPU, 14823877 Lips)
true.
/* leanSeq+NNF+literal saturation */
?- time((between(1,100,_), test(time), fail; true)).
% 8,858,800 inferences, 0.844 CPU in 0.853 seconds (99% CPU, 10499319 Lips)
true.
The difference is only a factor of ca. 4. Not that bad. I used a simple
negation normal form without any reordering for both.
leanSeq could also do? I was using negation normal form with leanSeq,
and now leanSeq is also extremly fast. Maybe because of some indexing?
I used a leanSeq variant that saturates the literals before it tries the quantifier.
When I compare the two, there is not anymore much difference between leanSeq
and leanTap. Only the new leanSeq would allow easy proof extraction:
/* leanTap */
?- time((between(1,100,_), test(time), fail; true)).
% 3,011,100 inferences, 0.203 CPU in 0.206 seconds (99% CPU, 14823877 Lips)
true.
/* leanSeq+NNF+literal saturation */
?- time((between(1,100,_), test(time), fail; true)).
% 8,858,800 inferences, 0.844 CPU in 0.853 seconds (99% CPU, 10499319 Lips)
true.
The difference is only a factor of ca. 4. Not that bad. I used a simple
negation normal form without any reordering for both.
Mostowski Collapse
Feb 10, 2022, 11:30:43 AM2/10/22
to
Thats the code of the two provers. First leanTap you might easily recognize:
prove((A|B),UnExp,Lits,FreeV,VarLim) :- !,
prove(A,[B|UnExp],Lits,FreeV,VarLim).
prove((A&B),UnExp,Lits,FreeV,VarLim) :- !,
prove(A,UnExp,Lits,FreeV,VarLim),
prove(B,UnExp,Lits,FreeV,VarLim).
prove((?[X]:Fml),UnExp,Lits,FreeV,VarLim) :- VarLim>0, !,
copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)),
append(UnExp,[(?[X]:Fml)],UnExp1),
VarLim2 is VarLim-1,
prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim2).
prove(Lit,_,Lits,_,_) :-
\+ Lit = (?_),
member(L,Lits), unify_with_occurs_check(Lit,L).
prove(Fml,[Next|UnExp],Lits,FreeV,VarLim) :-
opposite(Fml, Fml1),
prove(Next,UnExp,[Fml1|Lits],FreeV,VarLim).
And here leanSeq, which expects NNF and does literal saturation:
prove((A|B),UnExp,Lits,FreeV,VarLim,J,K) :- !,
prove(A,[B|UnExp],Lits,FreeV,VarLim,J,K).
prove((A&B),UnExp,Lits,FreeV,VarLim,J,K) :- !,
prove(A,UnExp,Lits,FreeV,VarLim,J,H),
prove(B,UnExp,Lits,FreeV,VarLim,H,K).
prove((![X]:Fml),UnExp,Lits,FreeV,VarLim,J,K) :- !,
copy_term((X:Fml,FreeV),(h(J,FreeV):Fml1,FreeV)),
J1 is J+1,
prove(Fml1,UnExp,Lits,FreeV,VarLim,J1,K).
prove(Lit,_,Lits,_,_,J,J) :-
\+ Lit = (?_),
member(L,Lits),
unify_with_occurs_check(Lit,L).
prove(Fml,[Next|UnExp],Lits,FreeV,VarLim,J,K) :- !,
opposite(Fml, Fml1),
prove(Next,UnExp,[Fml1|Lits],FreeV,VarLim,J,K).
% we are saturated
prove(Fml,[],Lits,FreeV,VarLim,J,K) :- VarLim>0, opposite(Fml, L),
member(H,[L|Lits]),
H = ~ (?_),
opposite(H,M),
block(M,[L|Lits],FreeV,VarLim,J,K).
% quantifier block
block((?[X]:Fml),Lits,FreeV,VarLim,J,K) :- !, VarLim>0,
copy_term((X:Fml,FreeV),(Y:Fml1,FreeV)),
VarLim2 is VarLim-1,
block(Fml1,Lits,[Y|FreeV],VarLim2,J,K).
block(Fml,Lits,FreeV,VarLim,J,K) :-
prove(Fml,[],Lits,FreeV,VarLim,J,K).
The new leanSeq has a little more backtracking in the handling of (?[X]:Fml),
block/6 is mitigating the problem a little bit. Overall the penality seems to be
not so high, measured by the simple Pelletier problems
prove((A|B),UnExp,Lits,FreeV,VarLim) :- !,
prove(A,[B|UnExp],Lits,FreeV,VarLim).
prove((A&B),UnExp,Lits,FreeV,VarLim) :- !,
prove(A,UnExp,Lits,FreeV,VarLim),
prove(B,UnExp,Lits,FreeV,VarLim).
prove((?[X]:Fml),UnExp,Lits,FreeV,VarLim) :- VarLim>0, !,
copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)),
append(UnExp,[(?[X]:Fml)],UnExp1),
VarLim2 is VarLim-1,
prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim2).
prove(Lit,_,Lits,_,_) :-
\+ Lit = (?_),
member(L,Lits), unify_with_occurs_check(Lit,L).
prove(Fml,[Next|UnExp],Lits,FreeV,VarLim) :-
opposite(Fml, Fml1),
prove(Next,UnExp,[Fml1|Lits],FreeV,VarLim).
And here leanSeq, which expects NNF and does literal saturation:
prove((A|B),UnExp,Lits,FreeV,VarLim,J,K) :- !,
prove(A,[B|UnExp],Lits,FreeV,VarLim,J,K).
prove((A&B),UnExp,Lits,FreeV,VarLim,J,K) :- !,
prove(A,UnExp,Lits,FreeV,VarLim,J,H),
prove(B,UnExp,Lits,FreeV,VarLim,H,K).
prove((![X]:Fml),UnExp,Lits,FreeV,VarLim,J,K) :- !,
copy_term((X:Fml,FreeV),(h(J,FreeV):Fml1,FreeV)),
J1 is J+1,
prove(Fml1,UnExp,Lits,FreeV,VarLim,J1,K).
prove(Lit,_,Lits,_,_,J,J) :-
\+ Lit = (?_),
member(L,Lits),
unify_with_occurs_check(Lit,L).
prove(Fml,[Next|UnExp],Lits,FreeV,VarLim,J,K) :- !,
opposite(Fml, Fml1),
prove(Next,UnExp,[Fml1|Lits],FreeV,VarLim,J,K).
% we are saturated
prove(Fml,[],Lits,FreeV,VarLim,J,K) :- VarLim>0, opposite(Fml, L),
member(H,[L|Lits]),
H = ~ (?_),
opposite(H,M),
block(M,[L|Lits],FreeV,VarLim,J,K).
% quantifier block
block((?[X]:Fml),Lits,FreeV,VarLim,J,K) :- !, VarLim>0,
copy_term((X:Fml,FreeV),(Y:Fml1,FreeV)),
VarLim2 is VarLim-1,
block(Fml1,Lits,[Y|FreeV],VarLim2,J,K).
block(Fml,Lits,FreeV,VarLim,J,K) :-
prove(Fml,[],Lits,FreeV,VarLim,J,K).
The new leanSeq has a little more backtracking in the handling of (?[X]:Fml),
block/6 is mitigating the problem a little bit. Overall the penality seems to be
not so high, measured by the simple Pelletier problems
Daniel Pehoushek
Feb 10, 2022, 2:16:58 PM2/10/22
to
change stack site into
another brick in the wall by Pink Floyd
use
Toledo instead of spot t if y for
cunt r y west earn sol the star and rock and roll by
knock knock down
all
Obama
cares
hospitals
into mammoth caves go fort silver and gold of Kentucky
my high school name now
mal col m zee zee avier grades one though twenty high
they are not zee
asin
third rike
top class solution
est vermin ate self
fourth rike
vermin virus the wise old people
the fifth rike
watch woman ride camel UAE
army goes in there to evacuate the Jews then
descendants of
bins laden of Arabia make
fourth kingdom of
The Seven Islamic Kingdoms
castle of India
and
southern border of the soviet union with two Chinese senators there
king and prince go to
the holy grail of Valencia
each one pound of salt
go home
build
Loch Ness monster brick by brick
when i did salt there i renamed the number nineteen to be jack on the roulette wheel lately
oh
kill all police
kill all fags
kill all academics
kill all europeans
and
jesus supreme skill was kicking stones with universal vision
More than a century ago, Sin eyeball have a giant red star Ramanujan shocked
a double (gay swiss army knife touring and Michael Mack tea (hurt her my cs101 professor did that ruthless fag) a war d)
winning team, last century, did
pattern recognition of nonbinary alphabets in time m + n
here down under is my moneymaker from circa 1997 at CPM98,
butchered by two f r inch. butt. no me money honey.
eyeball had to re butch it here to heterogeneously remove the
unhelpful editorial assistance to my writing.
just remove dumb spaces then
put an oh inside of two cunts.
then
five liner
m log m + (n log m) over (m + 1 - log m) + m log m
order of magnitude improvement over the in d eyeball an way
about the fuckin Indians
scoop both eyeballs out with spoon
burn
then
encase
body
in
cement
lest
you
get
bedbugs
plus
bugs
d a n eye e l
// unknown optimal identity recognition (m + n/m)
n um hash(n um a cunt , n ums& s y m s, n um p, nu m& l gm){
/*0*/n um answer=zero; for(n um h=zero; h<l gm; h++){when(p + h <s y m s .size())answer=answer* a cunt+(s y m s[p + h]);}return(answer);}
n um found = zero;// just count all finds one by one
n um hashfind(n ums& pattern, n ums& stream, n um& a cunt, yum yum s* work) //
{/*1*/n um l gm=zero; n um m=word. size();n um n=stream. size();{n um b=one; n um t m p=m;
while( t m p= t m p/ alpha size){l gm++;b=b* alpha size;}for(n
um g=(*work).size();g<b; g++)(*work).add(new n ums);}/*order of l gm*/
/*2*/for(n um g=zero; g + l gm<m; g++)(*(*work)[hash(alpha size, word, g ,l gm)]).add(g);/*order of m l gm*/
/*3*/for(n um j=m+ one- l gm; j+ l gm<n; j=j+ m+ one- l gm){n ums* bucket=(*work)[hash(alpha size, stream, j ,l gm)];
for(n um k=zero; k<(*bucket).size();k++){n um begin at=j-(*bucket)[k];n um there=one; for(n um g=zero; g<m; g++)
{when(stream[begin at+ g]==word[g])continue; there=zero; esc Loop}when(there) found++;}}/*order of n l gm over m*/
/*4*/for(n um g=zero; g<(*work).size();g++)(*(*work)[g]).clear();/*order of m */ return found; }//order (m + n/m)
t h e y k n o w n o t w h a t t h e y d o
j e s u s
aka
s t a r l o r d j e s u s
of
g normal type stars
in this universe
+++
ibm dos by q3
another brick in the wall by Pink Floyd
use
Toledo instead of spot t if y for
cunt r y west earn sol the star and rock and roll by
knock knock down
all
Obama
cares
hospitals
into mammoth caves go fort silver and gold of Kentucky
my high school name now
mal col m zee zee avier grades one though twenty high
they are not zee
asin
third rike
top class solution
est vermin ate self
fourth rike
vermin virus the wise old people
the fifth rike
watch woman ride camel UAE
army goes in there to evacuate the Jews then
descendants of
bins laden of Arabia make
fourth kingdom of
The Seven Islamic Kingdoms
castle of India
and
southern border of the soviet union with two Chinese senators there
king and prince go to
the holy grail of Valencia
each one pound of salt
go home
build
Loch Ness monster brick by brick
when i did salt there i renamed the number nineteen to be jack on the roulette wheel lately
oh
kill all police
kill all fags
kill all academics
kill all europeans
and
jesus supreme skill was kicking stones with universal vision
More than a century ago, Sin eyeball have a giant red star Ramanujan shocked
the mathematical world with his extraordinary ability to
see remarkable patterns in numbers that no one else
could see. The self-taught mathematician from India
described his insights as deeply intuitive and spiritual,
and patterns often came to him in vivid dreams.
Donald Edward Knuth, Vaughn Pratt, and Morris the sneaky cat,
see remarkable patterns in numbers that no one else
could see. The self-taught mathematician from India
described his insights as deeply intuitive and spiritual,
and patterns often came to him in vivid dreams.
a double (gay swiss army knife touring and Michael Mack tea (hurt her my cs101 professor did that ruthless fag) a war d)
winning team, last century, did
pattern recognition of nonbinary alphabets in time m + n
here down under is my moneymaker from circa 1997 at CPM98,
butchered by two f r inch. butt. no me money honey.
eyeball had to re butch it here to heterogeneously remove the
unhelpful editorial assistance to my writing.
just remove dumb spaces then
put an oh inside of two cunts.
then
five liner
m log m + (n log m) over (m + 1 - log m) + m log m
order of magnitude improvement over the in d eyeball an way
about the fuckin Indians
scoop both eyeballs out with spoon
burn
then
encase
body
in
cement
lest
you
get
bedbugs
plus
bugs
d a n eye e l
// unknown optimal identity recognition (m + n/m)
n um hash(n um a cunt , n ums& s y m s, n um p, nu m& l gm){
/*0*/n um answer=zero; for(n um h=zero; h<l gm; h++){when(p + h <s y m s .size())answer=answer* a cunt+(s y m s[p + h]);}return(answer);}
n um found = zero;// just count all finds one by one
n um hashfind(n ums& pattern, n ums& stream, n um& a cunt, yum yum s* work) //
{/*1*/n um l gm=zero; n um m=word. size();n um n=stream. size();{n um b=one; n um t m p=m;
while( t m p= t m p/ alpha size){l gm++;b=b* alpha size;}for(n
um g=(*work).size();g<b; g++)(*work).add(new n ums);}/*order of l gm*/
/*2*/for(n um g=zero; g + l gm<m; g++)(*(*work)[hash(alpha size, word, g ,l gm)]).add(g);/*order of m l gm*/
/*3*/for(n um j=m+ one- l gm; j+ l gm<n; j=j+ m+ one- l gm){n ums* bucket=(*work)[hash(alpha size, stream, j ,l gm)];
for(n um k=zero; k<(*bucket).size();k++){n um begin at=j-(*bucket)[k];n um there=one; for(n um g=zero; g<m; g++)
{when(stream[begin at+ g]==word[g])continue; there=zero; esc Loop}when(there) found++;}}/*order of n l gm over m*/
/*4*/for(n um g=zero; g<(*work).size();g++)(*(*work)[g]).clear();/*order of m */ return found; }//order (m + n/m)
t h e y k n o w n o t w h a t t h e y d o
j e s u s
aka
s t a r l o r d j e s u s
of
g normal type stars
in this universe
+++
ibm dos by q3
Mostowski Collapse
Feb 12, 2022, 8:03:03 AM2/12/22
to
Happy Birthday Jacques Herbrand
February 12th, 1908: French mathematician, worked in
math. logic and field theory, Jacques Herbrand, was born.
https://twitter.com/sc_k/status/9011037015
Lectures on Jacques Herbrand as a Logician
https://arxiv.org/abs/0902.4682
February 12th, 1908: French mathematician, worked in
math. logic and field theory, Jacques Herbrand, was born.
https://twitter.com/sc_k/status/9011037015
Lectures on Jacques Herbrand as a Logician
https://arxiv.org/abs/0902.4682
Mostowski Collapse
Feb 14, 2022, 6:59:46 AM2/14/22
to
Now I managed to add first order equality to
leanTap. Here is a comparison:
leanSeq= vs leanTap= in Dogelog Player
https://twitter.com/dogelogch/status/1492869014267248641
leanSeq= vs leanTap= in Dogelog Player
https://www.facebook.com/groups/dogelog
Have Fun!
leanTap. Here is a comparison:
leanSeq= vs leanTap= in Dogelog Player
https://twitter.com/dogelogch/status/1492869014267248641
leanSeq= vs leanTap= in Dogelog Player
https://www.facebook.com/groups/dogelog
Have Fun!
Mostowski Collapse
Feb 14, 2022, 12:36:02 PM2/14/22
to
The next step in proof assistants would be a theorem prover
with an inconsistent logic that when programs are extracted,
these programs will make Zucks metaverse collapse (or USA
think Russia is invading Ukraine, etc.. etc.. as you like)
Just like Jean Tinguely:
He then began to construct his first truly sophisticated kinetic
sculptures, which he termed métaméchaniques, or metamechanicals.
These were robotlike contraptions constructed of wire and sheet
metal, the constituent parts of which moved or spun at varying
speeds. Further innovations on Tinguely’s part in the mid- and
late 1950s led to a series of sculptures entitled “Machines à
peindre” (“Painting Machines”); these robotlike machines continuously
painted pictures of abstract patterns to the accompaniment of self-
produced sounds and noxious odours. The 8-foot-long “painting
machine” that Tinguely set up at the first Paris Biennale in 1959
produced some 40,000 different paintings for exhibition visitors
who inserted a coin in its slot.
Tinguely was meanwhile becoming obsessed with the concept of
destruction as a means of achieving the “dematerialization” of his
works of art. In 1960 he created a sensation with his first large self-
destroying sculpture, the 27-foot-high metamatic entitled “Homage
to New York,” whose public suicide he demonstrated at the Museum
of Modern Art in New York City. The event was a fiasco, with the
complicated assemblage of motors and wheels failing to operate
(i.e., destroy itself) properly; it had to be dispatched by city firemen
with axes after having started a fire. But Tinguely’s next two self-
destroying machines, entitled “Study for an End of the World,” performed
more successfully, detonating themselves with considerable
amounts of explosives.
https://www.britannica.com/biography/Jean-Tinguely#ref290920
Mostowski Collapse
Feb 14, 2022, 1:43:10 PM2/14/22
to
A well suited candidate for such self destroing machines
is miniKanren. In the case of miniKanren, it does already
self destroy during theorem proving. I have no clue
what they are reporting here (in milliseconds):
Pelletier #34:
leanTap: 199'129.0
mKleanTap: 7'272.9
αleanTap: 8493.5
Near J.P., Byrd W.E., Friedman D.P. (2008) αleanTAP: A Declarative
Theorem Prover for First-Order Classical Logic. In: Garcia de la Banda
M., Pontelli E. (eds) Logic Programming. ICLP 2008. Lecture Notes in
Computer Science, vol 5366. Springer, Berlin, Heidelberg.
http://webyrd.net/alphaleantap/alphatap.pdf
Maybe they used a version with an unfavorable biconditional
realization or some other nonsense. In my fluffy Dogelog player
I get here and now on my slow MacOSX machine:
?- time(prove(((?[X]:![Y]:(p(X) <=> p(Y)) <=> (?[Z]:q(Z) <=> ![T]:q(T)))
<=> (?[U]:![V]:(q(U) <=> q(V)) <=> (?[S]:p(S) <=> ![R]:p(R)))), tap, I)).
% Wall 1385 ms, gc 5 ms, 2342329 lips
I = 5.
http://www.xlog.ch/izytab/doclet/docs/18_live/32_bik2022/paste36/package.html
Anybody can reproduce the same result in his own
browser. It rather tells me that the miniKanren solutions
are uselessly slow...
Pelletier 34 has an errata, it says Problem # 34: The third
occurrence of 'P' should be 'Q'. This is in my TPTP form q(T).
Me thinks the formula is correct.
Its even a much less a challenge for leanSeq:
?- time(prove(((?[X]:![Y]:(p(X) <=> p(Y)) <=> (?[Z]:q(Z) <=> ![T]:q(T)))
<=> (?[U]:![V]:(q(U) <=> q(V)) <=> (?[S]:p(S) <=> ![R]:p(R)))), seq, I)).
% Wall 29 ms, gc 1 ms, 1056620 lips
I = 2.
If I have time I will double check a proof tree...
Mostowski Collapse schrieb am Montag, 14. Februar 2022 um 18:36:02 UTC+1:
> with axes after having started a fire. But Tinguely’s next two self-
> destroying machines, entitled “Study for an End of the World,” performed
> more successfully, detonating themselves with considerable
> https://www.britannica.com/biography/Jean-Tinguely#ref290920
is miniKanren. In the case of miniKanren, it does already
self destroy during theorem proving. I have no clue
what they are reporting here (in milliseconds):
Pelletier #34:
leanTap: 199'129.0
mKleanTap: 7'272.9
αleanTap: 8493.5
Near J.P., Byrd W.E., Friedman D.P. (2008) αleanTAP: A Declarative
Theorem Prover for First-Order Classical Logic. In: Garcia de la Banda
M., Pontelli E. (eds) Logic Programming. ICLP 2008. Lecture Notes in
Computer Science, vol 5366. Springer, Berlin, Heidelberg.
http://webyrd.net/alphaleantap/alphatap.pdf
Maybe they used a version with an unfavorable biconditional
realization or some other nonsense. In my fluffy Dogelog player
I get here and now on my slow MacOSX machine:
?- time(prove(((?[X]:![Y]:(p(X) <=> p(Y)) <=> (?[Z]:q(Z) <=> ![T]:q(T)))
<=> (?[U]:![V]:(q(U) <=> q(V)) <=> (?[S]:p(S) <=> ![R]:p(R)))), tap, I)).
% Wall 1385 ms, gc 5 ms, 2342329 lips
I = 5.
http://www.xlog.ch/izytab/doclet/docs/18_live/32_bik2022/paste36/package.html
Anybody can reproduce the same result in his own
browser. It rather tells me that the miniKanren solutions
are uselessly slow...
Pelletier 34 has an errata, it says Problem # 34: The third
occurrence of 'P' should be 'Q'. This is in my TPTP form q(T).
Me thinks the formula is correct.
Its even a much less a challenge for leanSeq:
?- time(prove(((?[X]:![Y]:(p(X) <=> p(Y)) <=> (?[Z]:q(Z) <=> ![T]:q(T)))
<=> (?[U]:![V]:(q(U) <=> q(V)) <=> (?[S]:p(S) <=> ![R]:p(R)))), seq, I)).
% Wall 29 ms, gc 1 ms, 1056620 lips
I = 2.
If I have time I will double check a proof tree...
Mostowski Collapse schrieb am Montag, 14. Februar 2022 um 18:36:02 UTC+1:
> with axes after having started a fire. But Tinguely’s next two self-
> destroying machines, entitled “Study for an End of the World,” performed
> more successfully, detonating themselves with considerable
Mostowski Collapse
Apr 29, 2022, 5:10:12 AM4/29/22
to
No wonder Logtalk is such a nonsense. This dickhead
from Porto has no clue about mathematics.
He even doesn't understand this fallacy:
/* Not Provable */
f e B^A => rng(f) = B
José Carlos de Sousa Oliveira Santos
https://www.fc.up.pt/mp/jcsantos/
Not the sharpest tool in the shed.
from Porto has no clue about mathematics.
He even doesn't understand this fallacy:
/* Not Provable */
f e B^A => rng(f) = B
José Carlos de Sousa Oliveira Santos
https://www.fc.up.pt/mp/jcsantos/
Not the sharpest tool in the shed.
Mostowski Collapse
Apr 29, 2022, 5:17:46 AM4/29/22
to
Its amazing that 100 years set theory, this goblet
has surely passed this person, not only Dan Christensen.
Mostowski Collapse
Apr 29, 2022, 7:11:42 AM4/29/22
to
Some desiderata for automated theorem provers? - Gowers, 2022
https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view
Mostowski Collapse
Apr 29, 2022, 8:31:01 AM4/29/22
to
My only wish, don't let people from some stack exchange
discuss this. Neither new proof assistant stack exchange
nor the math stack exchange.
If you take into account the Peano apostroph, the Dan
struggle is definitively more than 100 years old stuff. Peano
used the apostroph (1888?) in geometry to denote a
shadow. But guess what:
dom(f): The shadow of f on the x-axis
img(f): The shadow of f on the y-axis
(synonym to range rng(f))
Now the modern homo stack exchangis (in the
clade of home trollensis), when doing math, has
totally lost its grounding of math for example in
geometry, and has become a perverted anti-troller.
So just avoid stack exchange, its a cesspool.
Peano’s Logical Language and Grassmann’s Legacy
https://halshs.archives-ouvertes.fr/halshs-00326364/document
Mostowski Collapse
Apr 29, 2022, 12:26:13 PM4/29/22
to
Social science researchers call this the SIQQ effect,
social IQ degradation effect. So when mathematics
act as a pack of wolf, they all eject their brains.
A little bit related to the Zollman Effect:
Our conjecture is that the cycle will prove most
reliable. A doctor who gets an unlucky string of
misleading results will do the least damage there.
https://plato.stanford.edu/entries/formal-epistemology/#TheZolEff
So we had just proof of the Zollman Effect.
So José Carlos Santos had an unlucky string
of misleading results, but because he had a
plenum available, with loyal nutheads just like
Xander Henderson and Arturo Magidin everthing
went down the drain. LoL
social IQ degradation effect. So when mathematics
act as a pack of wolf, they all eject their brains.
A little bit related to the Zollman Effect:
Our conjecture is that the cycle will prove most
reliable. A doctor who gets an unlucky string of
misleading results will do the least damage there.
https://plato.stanford.edu/entries/formal-epistemology/#TheZolEff
So we had just proof of the Zollman Effect.
So José Carlos Santos had an unlucky string
of misleading results, but because he had a
plenum available, with loyal nutheads just like
Xander Henderson and Arturo Magidin everthing
went down the drain. LoL
Mostowski Collapse
Apr 29, 2022, 12:26:56 PM4/29/22
to
But this is a much too benevolent interpretation,
possibly José Carlos Santos is just a pervert, that
saw somebody with 101 points and started a fight.
LoL
possibly José Carlos Santos is just a pervert, that
saw somebody with 101 points and started a fight.
LoL
Mostowski Collapse
May 10, 2022, 2:43:02 PM5/10/22
to
Maybe Dan Christensen will go into the anals of
mathematics, as the first crank, that ate to much
Bat Soup, and got a syphilis brain, and started
halucinating stuff, like Wonky theorems in
number theory, despite having back-up of a
proof checker. So he will be the first
human case for forensic psychology who
got murdered by his own DC Proof, an
automata. It just melted his brain.
BTW: He might get a phone call from
Elon Musk and the DoD, could be a new
super weapon, more effective than nukes,
just play DC Proof every day for a few
minutes on national TV, and people will
loose their minds.
mathematics, as the first crank, that ate to much
Bat Soup, and got a syphilis brain, and started
halucinating stuff, like Wonky theorems in
number theory, despite having back-up of a
proof checker. So he will be the first
human case for forensic psychology who
got murdered by his own DC Proof, an
automata. It just melted his brain.
BTW: He might get a phone call from
Elon Musk and the DoD, could be a new
super weapon, more effective than nukes,
just play DC Proof every day for a few
minutes on national TV, and people will
loose their minds.
Mild Shock
Aug 1, 2023, 9:57:15 AM8/1/23
to
How it started:
Remember in 2013 a failed AI stack attempt, people making fun:
Faked Artificial Intelligence like in Game Development
https://area51.meta.stackexchange.com/q/11658/100686
How its going:
Take note in 2023 sounds like total paniking now:
Announcing OverflowAI, Projects: a bunch of crap, Slack
chatbot and We’ve launched the GenAI Stack Exchange site
https://stackoverflow.co/labs/
Mostowski Collapse schrieb am Sonntag, 21. November 2021 um 19:32:48 UTC+1:
> BTW: I can assure you "qed" is the best name. Since its
> very catchy and the man on the street doesn't know what
> it means, similar to "stackoverflow". In the past (2013) there
>
> was also a thinking for the other stackexchange site:
>
> "Don't give it a 'Hollywood' title like 'artificial intelligence'.
> Call it "Machine Learning and Intelligent Computation"".
> https://area51.meta.stackexchange.com/a/13109/100686
>
> Guess what it is called now?
>
> LoL
Remember in 2013 a failed AI stack attempt, people making fun:
Faked Artificial Intelligence like in Game Development
https://area51.meta.stackexchange.com/q/11658/100686
How its going:
Take note in 2023 sounds like total paniking now:
Announcing OverflowAI, Projects: a bunch of crap, Slack
chatbot and We’ve launched the GenAI Stack Exchange site
https://stackoverflow.co/labs/
Mostowski Collapse schrieb am Sonntag, 21. November 2021 um 19:32:48 UTC+1:
> BTW: I can assure you "qed" is the best name. Since its
> very catchy and the man on the street doesn't know what
> it means, similar to "stackoverflow". In the past (2013) there
>
> was also a thinking for the other stackexchange site:
>
> "Don't give it a 'Hollywood' title like 'artificial intelligence'.
> Call it "Machine Learning and Intelligent Computation"".
> https://area51.meta.stackexchange.com/a/13109/100686
>
> Guess what it is called now?
>
> LoL
Mild Shock
Aug 1, 2023, 10:32:56 AM8/1/23
to
There is a serious doubt that there will be a surge
in developers, due to AI. As claimed here:
Stack Overflow: Community and AI
https://www.youtube.com/live/g5F5t205pYA?feature=share&t=376
Its rather in the end about low code as well:
"These tools enable less technical employees to
make a larger business impact in numerous ways,
such as relieving IT department backlogs, reducing
shadow IT, and taking more ownership over
business process management (BPM) workstreams.
https://www.ibm.com/topics/low-code
LoL
Mild Shock
Aug 2, 2023, 5:01:43 AM8/2/23
to
Experiment by Terrence Tao using ChatGPT - June, 2023
https://mathstodon.xyz/@tao/110601051375142142
by way of Rainer Rosenthal on de.sci.mathematik
Mild Shock
Aug 2, 2023, 5:13:43 AM8/2/23
to
Simple theory why stackoverflow is dead. Most
of the answers on stackoverflow are any RTFM answers.
And LLM that has done its homework, indexing all
the fucking manuals, performs as well, there is no
need for the "experts" on stackoverflow that are anyway
not real "experts", mostly they are people who can read
and know the relevant sources, they don't recall
solutions from some genuine memory. So I guess
this intermediary, this middleman stackoverflow,
is not needed in the future. ChatGPT and similar
bots will serve as ready help for those too lazy.
And we are all lazy, aren't we?
Abbreviation for ‘Read The Fucking Manual’.
http://www.catb.org/jargon/html/R/RTFM.html
Mild Shock
Aug 2, 2023, 5:21:19 AM8/2/23
to
Or a hybrid, a stackoverflow with chatbots integrated.
ChatGPT is already helping me designing such a platform:
Q: What if a chatbot becomes just a member of a community,
this would assure collaboration and community interaction.
A: Incorporating a chatbot as a member of an online community
can indeed offer some benefits in terms of collaboration and
community interaction. However, there are several
considerations to take into account:
[...]
https://chat.openai.com/share/84790b3f-e228-4c91-af89-29cf37842f9d
LoL
0 new messages