Can cognitive architectures (CLARION, SOAR, ACT-R, others) be used for creative mathematical reasoning? As far as I understand, then it is the best to encode formal mathematical knowledge in the languages of proof assistants like Coq (CIC - Calculus of Inductive Constructions), Lean, Isabelle/HOL, Mizar. But those proof assistants require manual/creative human invovlement for the tasks like:

  • concept/new definition creation, creation of theories;
  • formulation of theorems and lemmas (to be proved by proof assistant);
  • selection of arguments, selection of proof tactics, invention of new proof tactics;
  • goal definition and direction definition in forward reasoning/chaining, e.g. in creating more or less expanded full consequence set from selected set of theorems.

All these tasks require creativity, human-level determination and goal evaluation/selection. So - can these listed activies be done by the cognitive architectures or other computational creativity tools? Is such integration of hard/soft formal/creative proof-assistant/cognitive-architecture tools and approaches under research and development? Is there scientific literature about such integration specifically and about application of cognitive architectures to doing math generally?

Such integration and application can be of immense benefit to humanity. E.g. for the automatic generation and analysis of the algorithms for the optimization, robotics, scheduling etc. For the automatic search of new logics and for the automatic self-improvement of proof assistants and cognitive architectures themselves.

  • $\begingroup$ I've been poking around SOAR recently. I think it needs a state-space definition, so definite training wheels. I am unfamiliar with the proof assistants, so thanks for the list. I hope to look them up. $\endgroup$ – EngrStudent Apr 16 '20 at 19:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.