Re: Transactions: good or bad?
From: Costin Cozianu <c_cozianu_at_hotmail.com>
Date: Sun, 15 Jun 2003 08:49:10 -0700
Message-ID: <bci4e1$jej56$1_at_ID-152540.news.dfncis.de>
>
>
> I don't see what that has to do with automated theorem proving, which
> computers do now.
>
> With all due respect, Costin, you are talking past Alfredo, and you have
> turned your discussion with Alfredo into a pissing match. Computers do not
> have to think in order to prove theorems. They prove theorems without
> thinking because "thinking" is the word we use to describe how brains--not
> computers--solve problems just as "swimming" is the word we use to describe
> how animals--not submarines--move through water.
>
>
>
>
>
> I disagree.
>
>
>
>
>
> The one we all live in where computers actually prove theorems every day.
>
>
>
>
>
> Costin, you were wrong. Have the balls to admit it.
>
>
>
>
>
> For now. Before long, computers will create humans. Or have you not been
> following the advances in genetic engineering and sequencing?
>
>
>
>
>
> Yes. It does not prevent computers from proving theorems--including on
> occasion that a given class of programs will halt. There are plenty of
> conjectures that humans have never proved nor disproved and some that we may
> never prove or disprove. The same is as true for computers as it is for
> humans, and the halting problem applies to humans as much as it applies to
> computers.
>
>
>
>
>
> As are computers. Did you not pay attention to the part in the article cited
> earlier where the key strategy was to apply previously proved theorems? In
> other words, the computer creates the tools necessary for a proof.
>
>
Received on Sun Jun 15 2003 - 17:49:10 CEST
Date: Sun, 15 Jun 2003 08:49:10 -0700
Message-ID: <bci4e1$jej56$1_at_ID-152540.news.dfncis.de>
Bob,
Your "I disagree.Period." style has been noted.
Cheers,
Costin
Bob Badour wrote:
> "Costin Cozianu" <c_cozianu_at_hotmail.com> wrote in message
> news:bcfed9$idmcu$1_at_ID-152540.news.dfncis.de...
>
>>Alfredo Novoa wrote: >><snip ... > >> >>>What are neurons if not little computers? >>> >> >>You don't know that they are computers. As a matter of fact now computer >>has come even remoteyl close to what neurons can do. >> >>Nor even is there any scientific theory that might give us a hint that >>we'll be able to construct intelligent computers.
>
>
> I don't see what that has to do with automated theorem proving, which
> computers do now.
>
> With all due respect, Costin, you are talking past Alfredo, and you have
> turned your discussion with Alfredo into a pissing match. Computers do not
> have to think in order to prove theorems. They prove theorems without
> thinking because "thinking" is the word we use to describe how brains--not
> computers--solve problems just as "swimming" is the word we use to describe
> how animals--not submarines--move through water.
>
>
>
>>>>According to people like Dijkstra, Girard and others, this alone should >>>>allow you to draw the conclusions that computers "don't think". >>> >>> >>>But a computer does not need to think in order to prove a theorem or >>>to find a stalemate in five movements. >> >>Exactly he only neeeds to compute. In order to prove Pythagora's theorem >>you have to think.
>
>
> I disagree.
>
>
>
>>>>Computers can help people prove theorems, solve problems,etc, it will >>>>never be the caser that computers (the way we understand them now) will >>>>create mathematics. >>> >>> >>>I still don't see any argument. But you are now talking about creating >>>mathematics. Your former assertion was computers can not prove >>>theorems and is evident it is against reality. >>> >> >>Against what reality ?
>
>
> The one we all live in where computers actually prove theorems every day.
>
>
>
>>>Talking a little about databases :-) >>> >>>"The response to a query is a theorem. The process of deriving the >>>theorem from the axioms is a proof. The proof is made by manipulating >>>symbols according to agreed mathematical rules. The proof [that, is >>>the query result!] is as sound and consistent as the rules >>>are."(emphasis mine). A DBMS, then, is a deductive logic system: it >>>derives new facts from a set of asserted facts.<snip>" >>> >>>http://www.pgro.uk7.net/fp1e.htm >>> >> >>It has no bearing on the discussion. A database is pre-programmed for >>certain calculations. That's nto the same with creating proofs, which is >>how the discussion started.
>
>
> Costin, you were wrong. Have the balls to admit it.
>
>
>
>>>>Yes, sure. I see a lot of proof checkers, symbolic calculation engines, >>>>etc. Those are fine pieces of software. Most of them rely heavily on >>>>essential human input inm being able to "prove". >>> >>> >>>Proof checkers and proof makers. You see only what you want to see. >>> >>>Most of human proof makers also rely heavily on other human inputs. I >>>don't see the problem. >>> >> >>The difference is that humans create mathematics. Computers do not. >>Humans create computers.
>
>
> For now. Before long, computers will create humans. Or have you not been
> following the advances in genetic engineering and sequencing?
>
>
>
>>>Human lemma selection is not essential but it saves a lot of search >>>time. Only axioms and rules are essential inputs. >>> >> >>Do you know the Halting problem ?
>
>
> Yes. It does not prevent computers from proving theorems--including on
> occasion that a given class of programs will halt. There are plenty of
> conjectures that humans have never proved nor disproved and some that we may
> never prove or disprove. The same is as true for computers as it is for
> humans, and the halting problem applies to humans as much as it applies to
> computers.
>
>
>
>>>>Otherwise a computer is not able to decide when he's on a wrong, >>>>infinite path (aka the Halting Problem). >>> >>> >>>It is not an unsolvable problem. Humans have similar problems >>>sometimes. >>> >>>Humans are not near of being perfect theorem provers either. >>> >> >>No. Humans are creative theorem provers.
>
>
> As are computers. Did you not pay attention to the part in the article cited
> earlier where the key strategy was to apply previously proved theorems? In
> other words, the computer creates the tools necessary for a proof.
>
>
Received on Sun Jun 15 2003 - 17:49:10 CEST