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, -- 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 [email protected]. To post to this group, send email to [email protected]. 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.
