Resource Guided Concurrent Deduction
Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge · 2000
Our poster proposes an architecture for resource guided concurrent mechanised deduction which is motivated by some findings in cognitive science. Our architecture particularly reflects Hadamard’s “Psychology of Invention” [Hadamard44]. In his study Hadamard describes the predominant rôle of the unconsciousness when humans try to solve hard mathematical problems. He explains this phenomenon by its most important feature, namely that it can make (and indeed makes) use of concurrent search (whereas conscious thought cannot be concurrent), see p. 22 Hadamard (1944): “Therefore, we see that the unconscious has the important property of being manifold; several and probably many things can and do occur in it simultaneously. This contrasts with the conscious ego which is unique. We also see that this multiplicity of the unconscious enables it to carry