RE: Calculemus

From: Ben Goertzel (
Date: Tue Nov 09 2004 - 17:56:23 MST

Christian Szegedy wrote:
> I strongly believe that mathematical deduction and
> mathematical optimization could be the cornerstones
> of an efficient AI architecture on current hardware,

Christian, it would be great if you'd enlarge on this point.

I agree that deduction and optimization, in general, are key aspects of

However, it seems to me that most of the deduction the mind does is
probabilistic/uncertain in nature, and also much of it involves peculiar
temporal logic, so that standard crisp time-free mathematical deduction
isn't all *that* useful for AI.

And, it seems to me that the optimization occurring in the mind is a mix of
general-purpose *stochastic* optimization with specialized, domain-tuned
optimization algorithms (dealing with optimization in domains like visual
perception, arm movement, language parsing, etc.).

So I'm wondering if you've thought through any of the details of how to make
an AI based on mathematical deduction of the form used in contemporary
theorem-provers, and mathematical optimization of the form used in
contemporary computer algebra systems.

I can't deny that it might be possible, but I don't see it very clearly....

Regarding theorem-provers, for instance, the truth is that contemporary
theorem-provers use very oversimplistic inference control strategies. As an
example, the Otter theorem-prover, which is an excellent system compared to
most of the competitors, basically does only proofs by contradiction, and
deals with existential quantifiers solely by Skolemizing them out (which
only works in the context of proofs by contradiction and other special
cases). This kind of control strategy appears to bear no relevance to how
any adaptive, autonomous cognitive system would reason (presumably such
systems would reason by combining crisp deductive reasoning with
uncertain-inference-driven inductive and abductive reasoning and speculative

-- Ben G

This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:50 MDT