Researchers of reasoning in computer science and psychology are estranged siblings. The tools they use to investigate patterns of inference seldom overlap, because the goals of each group di er. A computer scientist's primary goal is to e ciently engineer systems based on logical calculi. But, human reasoning systematically violates the constraints imposed by orthodox logic. One logician described the disparity between logical systems and the everyday inferences they are intended to capture as \one of the greatest scandals of human existence" [1]. And so the psychological objective is to discover patterns of reasoning in humans, both normative and fallacious, with the ultimate goal of developing theories capable of predicting human inference. Despite their diverging purposes, computer scientists and psychologists face similar theoretical challenges: how is knowledge represented and integrated into reasoning processes? What constitutes a normative inference? Why are some inferences more di cult than others? Human reasoning is predictably irrational, but it can also be more productive, exible, and capable than current automated reasoning systems. Indeed, as some researchers argue, certain kinds of inference { such as reasoning about defaults, non-monotonic inference, explanatory reasoning, and conditional inference { cannot be characterized without reference to how humans make them [14, 16]. A keen understanding of human reasoning therefore has both psychological and computational value. Present day automated reasoning systems do not reason the way humans do { which may explain their success as inferential tools. The productivity of automated theorem provers (ATPs) has advanced by orders of magnitude since McCune's famous solution to the Robbins problem [13]. ATPs regularly compete against one another at international competitions to e ciently yield proofs of thousands of reasoning problems. For instance, the ATPs that entered the 2004 theorem-proving competition at the annual Conference on Automated Deduction (CADE) [18] were designed to solve two thousand eligible problems. At the same competition ten years later, the number of eligible problems grew to fteen thousand [17]. As a result of prolonged development, ATPs now routinely serve as productive analytical tools, and they are instrumental in diverse applications, such as the veri cation of transportation systems, electrical circuitry, and automation systems. But, ATPs are designed to carry out just one inferential task, i.e., they operate by deriving a valid proof of a conclusion from a given set of premises. This
design constraint allows systems to lter out invalid inferences that may corrupt
further processing, but it represents a stark divergence from human thinking.
Humans do not spontaneously construct logical proofs when they reason [
mReasoner is a novel automated reasoning system [
In sum, mReasoner is a cognitively plausible automated reasoning system. It eschews logical formalisms in favor of mental models, i.e., discrete, iconic representations of possibilities. The system serves as an analytical tool that mimics both the frailties of human reasoning, e.g., systematic errors, as well as strengths of human inference, e.g., the ability to spontaneously generate relevant conclusions. Future applications in arti cial intelligence and computer science will demand automated reasoning systems that interact with human reasoners. Hence, mReasoner { and systems like it { provides a foundation for those interactions. Acknowledgments I am most indebted to my longtime mentor and collaborator, Phil JohnsonLaird, for his infectious enthusiasm, perseverance, and creativity. The work I've described would have been impossible without many conversations with Selmer Bringsjord, my mentor in logic, and Greg Trafton, whose abilities in computational cognitive modeling continue to inspire. Finally, I thank Paul Bello, Ruth Byrne, Monica Bucciarelli, Geo Goodwin, Tony Harrison, Laura Hiatt, Max Lotstein, Robert Mackiewicz, Isabel Orenes, and Marco Ragni for their comments and criticisms. 17. Geo Sutcli e. The CADE-24 automated theorem proving system competition{
CASC-24. AI Communications, 27(4):405{416, 2014. 18. Geo Sutcli e and Christian Suttner. The CADE-19 ATP system competition. AI Communications, 17(3):103{110, 2004.