Can AGI be of help for solving mathematical and engineering problems?

[Alex]

It is said in one of Goertzel's book that scientific data analysis and theorem proving probably can be done more efficiently outside the cognitive cycle of OpenCog. My question is - can AGI contribute towards solving engineering problems and proving mathematical theorems? From the one side the current focus of AGI is to replicate human behavior, motivations, emotions and (bounded and sometimes irrational) reasoning. From the other side - we cannot say that AGI system is complete if it can not do what bright human individuals can do - i.e. - prove theorems and introduce new mathematical concepts and theories. So - AGI should focus also on automatic solutions of the engineering and mathematical problems.

Currently I see the following tasks ahead in this direction:

- OpenCog should replace existing mathematical systems, like Mizar, by (automatic) translation of Mizar libraries into AtomSpaces

- OpenCog should implement more general and creative automatic theorem and proof search procedures, stress on creative (the synergy from artistic creativity can be employed)

- OpenCog should be adapted for the automatic translation of the inferred theories into human language and more accessible texbook forms, employing analogies, jokes and stories about applications and motivations

- OpenCog should be made ready to accept natural language input of mathematical texts and automatic processing of them, automatic addition to the relevant AtomSpaces. Also meta-level learning, reasoning and searching procedues should be read from the human-language texts and added to the AtomSpaces.

To achieve this agenda I see necessary to do the following tasks:

- decide how AtomSpaces can be used for representation of mathematical facts, algorithms and search techniques

- improve natural language processing, understanding and input/output.

AGI should win humans in theorem proving as well. In fact - automatic discovery and application of engineering knowledge should be one of the main application areas of AGI. Even today many computer systems that are necessary for humanity are too complex to be programmed and maintained by human. Search of better optimization algorithms is another necessity whose results can be very beneficial.

A,

[Ben Goertzel]

Representing math in the Atomspace is not problematic. The challenge
here is scalable control of uncertain inference (PLN), which will then
enable scalable control of crisp mathematical inference.... I think
we know how to make scalable PLN inference control work, but it's not
that simple (the correct approach, I think, is to mine patterns among
successful simple inferences, and then use these patterns to guide
rule and premise selection for more complex inferences). Theorem
proving would be an awesome test case to use while developing scalable
inference control, but it's not the direction we plan on pursuing in
the near future (unless things change!) as it is not what most
preoccupies our current funding sources...

ben

> --
> You received this message because you are subscribed to the Google Groups
> "opencog" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to opencog+u...@googlegroups.com.
> To post to this group, send email to ope...@googlegroups.com.
> Visit this group at https://groups.google.com/group/opencog.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/opencog/121bc616-b9e4-4927-95a2-4a393ed7075b%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.



--
Ben Goertzel, PhD
http://goertzel.org

“I tell my students, when you go to these meetings, see what direction
everyone is headed, so you can go in the opposite direction. Don’t
polish the brass on the bandwagon.” – V. S. Ramachandran