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 On Sun, Dec 11, 2016 at 10:50 PM, Alex <[email protected]> wrote: > 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. -- 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 -- 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/CACYTDBfCX9M9rjwvrN3VGhYp3A81%2B9CBqeyjVyaz_2uAP%3DeQ5g%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
