Re: Transactions: good or bad?

"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 Sat Jun 14 2003 - 20:00:07 CEST