I propose that the notion of cognitive state be broadened from the current predicate-symbolic, Language-of-Thought framework to a multi-modal one, where perception and kinesthetic modalities participate in thinking. In contrast to the roles assigned to perception and motor activities as modules external to central cognition in the currently dominant theories in AI and Cognitive Science, in the proposed approach, central cognition incorporates parts of the perceptual machinery. I motivate and describe the proposal schematically, and describe the implementation of a bimodal version in which a diagrammatic representation component is added to the cognitive state. The proposal explains our rich multimodal internal experience, and can be a key step in the realization of embodied agents. The proposed multimodal cognitive state can significantly enhance the agent's problem solving. Note: Memory, as well as the information retrieved from memory and from perception, represented in a predicate-symbolic form.

We discuss the representation of knowledge and of belief from the viewpoint of decision theory. While the Bayesian approach enjoys general-purpose applicability and axiomatic foundations, it suffers from several drawbacks. In particular, it does not model the belief formation process, and does not relate beliefs to evidence. We survey alternative approaches, and focus on formal model of casebased prediction and case-based decisions. A formal model of belief and knowledge representation needs to address several questions. The most basic ones are: (i) how do we represent knowledge?

A CASE-BASED MODEL OF CREATIVITY SCOT'[" R. TURNER Department of Computer Science University of California, Los Angeles Los Angeles CA 90024 USA Abstract Creativity - creating new solutions to problems - is an integral part of the problem-solving process. This paper presents a cognitive model of creativity in which a case-based problem-solver is augmented with (1) a creative drive and (2) a set of creativity heuristics. New solutions are discovered by solving a slightly different problem and adapting that solution to the original problem. By repeating this process, a creative problem-solver can discover new solutions that are novel, useful and very different from known solutions. This model has been implemented in a computer program called MINSTREL. MINSTREL has been used for planning and problem-solving, to tell stories, and to invent mechanical devices. 1 Introduction Creativity is an important element of human cognition. We all invent on a daily basis: we fix cars using spare change and bailing wire, invent jokes based on the latest domestic crisis, and make up bedtime stories for our children. The ability to invent original, useful solutions to problems is a fundamental process of human thought. To understand human cognition, we must understand the processes of creativity: the goals that drive people to create and the mechanisms they use to invent novel and useful solutions to their problems. This paper presents a model of creative reasoning as an extension to case-based problem-solving.

We propose an abductive diagnosis theory that integrates probabilistic, causal and taxonomic knowledge. Probabilistic knowledge allows us to select the most likely explanation; causal knowledge allows us to make reasonable independence assumptions; taxonomic knowledge allows causation to be modeled at different levels of detail, and allows observations be described in different levels of precision. Unlike most other approaches where a causal explanation is a hypothesis that one or more causative events occurred, we define an explanation of a set of observations to be an occurrence of a chain of causation events. These causation events constitute a scenario where all the observations are true. We show that the probabilities of the scenarios can be computed from the conditional probabilities of the causation events. Abductive reasoning is inherently complex even if only modest expressive power is allowed. However, our abduction algorithm is exponential only in the number of observations to be explained, and is polynomial in the size of the knowledge base. This contrasts with many other abduction procedures that are exponential in the size of the knowledge base.

Bright, Curtis, Kotsireas, Ilias, Ganesh, Vijay

Over the last few decades, many distinct lines of research aimed at automating mathematics have been developed, including computer algebra systems (CASs) for mathematical modelling, automated theorem provers for first-order logic, SAT/SMT solvers aimed at program verification, and higher-order proof assistants for checking mathematical proofs. More recently, some of these lines of research have started to converge in complementary ways. One success story is the combination of SAT solvers and CASs (SAT+CAS) aimed at resolving mathematical conjectures. Many conjectures in pure and applied mathematics are not amenable to traditional proof methods. Instead, they are best addressed via computational methods that involve very large combinatorial search spaces. SAT solvers are powerful methods to search through such large combinatorial spaces---consequently, many problems from a variety of mathematical domains have been reduced to SAT in an attempt to resolve them. However, solvers traditionally lack deep repositories of mathematical domain knowledge that can be crucial to pruning such large search spaces. By contrast, CASs are deep repositories of mathematical knowledge but lack efficient general search capabilities. By combining the search power of SAT with the deep mathematical knowledge in CASs we can solve many problems in mathematics that no other known methods seem capable of solving. We demonstrate the success of the SAT+CAS paradigm by highlighting many conjectures that have been disproven, verified, or partially verified using our tool MathCheck. These successes indicate that the paradigm is positioned to become a standard method for solving problems requiring both a significant amount of search and deep mathematical reasoning. For example, the SAT+CAS paradigm has recently been used by Heule, Kauers, and Seidl to find many new algorithms for $3\times3$ matrix multiplication.