Mechanisms in Behavior," John McCarthy became one of the first computer scientists who pioneered the formalization of commonsense reasoning. In 1955, just one year prior to the Dartmouth conference, he had coined the term "artificial intelligence." McCarthy proposed a system program, the so-called "advice taker," which
will have available to it a fairly wide class of immediate logical consequences of anything it is told and its previous knowledge...We shall therefore say that a program has common sense if it automatically deduces for itself a sufficiently wide class of immediate consequences of anything it is told and what it already knows.2
In contrast to reasoning systems which were understood as theorem-proving systems in a formal logic environment, his definition of common sense makes the handling of knowledge a central issue. Inspired by this proposition, in the following decades a variety of approaches to formulate commonsense reasoning have subsequently emerged. Most of these approaches focus on logical aspects and assumed that the knowledge necessary to solve a particular problem was already formalized and made available to the reasoner. More recently, Ronald Brachmann and Hector Levesque propose to rethink the programming approach in artificial intelligence by including commonsense capabilities. They argue that
having common sense is substantially more than having commonsense knowledge. At the very least it is the appropriate and timely application of this knowledge that is critical.3
In contrast to a purely logical approach, where all necessary axioms are fed into the reasoner—as it is proposed by McCarthy—they are demanding a memory-based approach, that is apt of addressing the question
How does an agent decide which chunks of knowledge to look at next, how they should combine with other chunks of knowledge, when to go back for another try, and even when to give up and try something different? [NSC 3]
2 John McCarthy, "Programs with Common Sens," in Formalizing Common Sense: Papers by John McCarthy, ed. Vladimir Lifschitz, Norwood, NJ: Ablex Publishing Corporation 1990, pp. 9-20, here p. 9.
3 Ronald J. Brachman and Hector J. Levesque, "Toward A New Science of Common Sense," arXiv 2112.12754v2 (6 February 2022), 1-6, here p. 3. [Henceforth cited as NSC]
determine which aspects of available data are relevant to the problem at hand. Hence, I propose a solution to this problem by using word embeddings, which is a method for integrating the meaning of symbols that are to be used in logical problem descriptions.
Automated Reasoning
Automated reasoning is one of the most traditional sub-disciplines of artificial intelligence and has been considered as being an important sub-discipline since artificial intelligence's very beginning. The methods for developing powerful and efficient inference systems are based on calculi of formal logic. John Alan Robinson's resolution calculus certainly represented an important starting point for the development of modern efficient proof procedures; subsequently many other calculi for various logics have been developed and applied. To further this end, sophisticated web repositories offer a library of problems for automated theorem proving systems. These depositories distinguish between and explain different problem classes and different logics, provide a comprehensive overview of current logical systems, and offer online access to state-of-the-art reasoning systems.
There are many applications and success stories with respect to automated reasoning. For instance, mathematical theorems can be proven automatically or with the help of deduction systems (such as the Kepler conjecture or Boolean Robbins algebra) and the verification of soft- and hardware systems has become a very relevant commercial domain.
An interesting application domain is to use first-order logic reasoning in order to solve commonsense problems that are usually formulated in natural language and can be easily solved by humans. In order to solve these problems in an artificial environment, one must translate it into a logical formula and feed it, along with background knowledge about the world, into the device which is now dubbed "the reasoner." This process is discussed in greater detail in the following sections.
Human Reasoning
When it comes to making simple everyday deductions, humans can do so effortlessly. However, automated reasoners often encounter computational procedure challenges when attempting to do the same. Inspired by the 1948 Caltech Hixon Symposium on "Cerebral
