Re: Transactions: good or bad?

Costin Cozianu <c_cozianu_at_hotmail.com> wrote in message news:<bccvvt$hsj03$1_at_ID-152540.news.dfncis.de>...

> >>That's non-sense. Go read good old Dijkstra if you can't read Girard in
> >>French.
> >
> >
> > Dijkstra has lots of writting, can you be more specifical?
> >
>
> Well, I don't have the exact number at hand but he wrote:
>
> "The question whether machines can think is as ill posed as the question
> whether submarines can swim."

I don't see any sound argument here or in the Girard paper. And the keyword here is "deduction" not thinking.

> > Artificial Intelligence: A Philosophical Introduction
> > by Jack Copeland (Paperback - November 1993)
> >
> > http://www.amazon.com/exec/obidos/tg/detail/-/063118385X/qid=1055496292/sr=1-1/ref=sr_1_1/104-6927268-4867955?v=glance&s=books
> >
> > There is a second hand copy for $10. It worths a while.
>
> No 10$ can compare with my time reading a good book versus my time
> reading a book that does not profit me.

Perhaps it does not profit you, but it is a very good and serious book. It sistematically debunks all the known arguments against the possibility of thinking machines.

What are neurons if not little computers?

> Any book with philosophy in its
> title raises my high level of suspicion.

Books like Rusell's Introduction to Mathematical Philosophy? :)

Sorry, it was a joke.

> To quote Dijsktra, again:
>
> "It seems there are societies in which philosophers still have some
> intellectual standing"

Philosophers like Rusell, Wittgenstein, Popper, etc?

> > Are you aware of the state of the art in automated proving?
>
> No, but I'm aware of the basics of logic and foundations of mathematics.

Saying that computers can not make proofs is like saying that computers can not play chess. It is an every day reality.

> 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. And computers don't think is not the same as computers can't think.

"Conjectures best suited to this approach are combinatorial problems in new areas of mathematics, where human intuitions are less well developed, [Wos,
1993]. The Robbins Algebra conjecture is a good example. Brute force search through all the
various possibilities is often an appropriate approach to such problems | and machines are much
better suited to brute force solutions than humans."

"A. Bundy. Survey of Automated Deduction 1999"

> 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.

It is very easy to create a software which proves not very trivial boolean algebra theorems.

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

> What a splendid "popularization of science" marketing paper written by a
> dumb journalist.

IMO it is a good science divulgation article in a prestigious (a little less prestigious this on days }:-) newspaper.

> 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.

Human lemma selection is not essential but it saves a lot of search time. Only axioms and rules are essential inputs.

> 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.

> Computers are very well equiped to perform calculations.

Computations is a better word.

> might be able to verify and sometimes even construct (albeit with
> essential human help) calculational proofs.

Finally you have admited that they construct proofs :-)

> To quote J.Y Girard
> "l'ordinateur n'est qu'un cyber-cretin".

A cyber-cretin which is able to beat Kasparov and to prove simple theorems and other not so simple.

Cretins are able to do useful things sometimes.

> It's provably impossible to create such a software that will take any
> sufficiently expressive formal system, a proposition in the system and
> *reliably* come up with the decision whether that proposition is a
> theorem or not.

Why?

Impossible is a strong word.

I don't think there is anything supernatural in the human mind. If we can think other machines also could. But you don't need to be self-concious in order to prove a theorem.

> As a matter of fact it seems from all the examples you presented that
> when they published the papers it was the humans who took credit for the
> precious few results that their computers could infer :) Isn't that
> kind of telling ?

Computer are not jealous, they don't protest :-)

> When I'll see the first computer to take the decision to submit a paper
> to a scientific journal, all by itself, then I'll reconsider my position.

You are mixing very different things.

Regards
  Alfredo Received on Sat Jun 14 2003 - 02:16:50 CEST