Logical reasoning
systems derive sound conclusions from formal declarative knowledge.
Such systems are usually defined by abstract rules of inference. For example,
the rule of modus ponens states that given P, and "P implies Q" (usually
written P 
Q), we can infer Q. Logical systems
have a rich history, starting with Greek syllogisms and continuing
through the work of many prominent mathematicians such as DESCARTES, Leibniz,
Boole, FREGE, Hilbert, Gödel, and
Cohen. (For a good discussion of the history of logical reasoning
systems, see Davis 1983.)
Logical reasoning provides a well-understood general method of symbolic COMPUTATION. Symbolic computation manipulates expressions involving variables. For example, a computer algebra system can simplify the expression x(x + 1) to x2+ x. The equation x(x + 1) = x 2 + x is true under any interpretation of x as a real number. Unlike numerical computation, symbolic computation derives truths that hold under a wide variety of interpretations and can be used when only partial information is given, for example, that x is some (unknown) real number. Logical inference systems can be used to perform symbolic computation with variables that range over conceptual domains such as sets, sequences, graphs, and computer data structures. Symbolic computation underlies essentially all modern efforts to formally verify computer hardware and software.
There are at least two ways in which symbolic inference is relevant to cognitive science. First, symbolic inference rules have traditionally been used as models of human mathematical reasoning. Second, symbolic computation also provides a model of certain commonsense inferences. For example, suppose one is given a bag of marbles and continues removing marbles from the bag for as long as it remains nonempty. People easily reach the conclusion that, barring unusual or magical circumstances, the bag will eventually become empty. They reach this conclusion without being told any particular number of marbles -- they reach a conclusion about an arbitrary set s. Computer systems for drawing such conclusions based on "visualization" do not currently work as well as approaches based on symbolic computation (McAllester 1991).
Here I will divide symbolic computation research into five general approaches. First are the so-called symbolic algebra systems such as Maple or Mathematica (Wolfram 1996), designed to manipulate expressions satisfying certain algebraic properties such as those satisfied by the real numbers. Although they have important applications in the physical sciences, these systems are not widely used for hardware or software verification and seem too specialized to provide plausible models of commonsense reasoning. Second are the symbolic model-checking systems (Burch et al. 1990), which perform symbolic inference where the variables range over finite sets such as the finite set of possible states of a certain piece of computer hardware. Although very effective for the finitary problems where they apply, these systems are too restricted for software verification and also seem too restricted to provide plausible models of commonsense reasoning. The remaining three approaches to symbolic computation all claim to be general purpose or domain independent. I will call these the "first-order approach," the "higher-order approach," and the "induction approach," respectively, and discuss each in turn.
The first-order approach is based on making inferences from axioms written in first-order LOGIC, which includes a wide variety of resolution and term-rewriting systems (Fitting 1996). For problems that can be naturally axiomatized in first-order logic, the first-order approach seems superior to other approaches. Unfortunately, most mathematical theorems and verification problems have no natural first-order formulation. Although detailed discussion of first-order logic and inference methods is beyond the scope of this entry, it is possible to give a somewhat superficial description of its limitations. First-order logic allows us to state properties of concepts, but not generally to define concepts. For example, suppose we want to describe the concept of a finite set. We can write a formal expression stating, "A set is finite if it is either empty or can be derived by adding a single element to some other finite set." Unfortunately, this statement does not uniquely determine the concept -- it is also true that "a set is countable if it is either empty or can be derived by adding a single element to some other countable set." Statements true of a concept often fail to uniquely specify them. Finiteness is not definable in first-order logic. The bag of marbles inference mentioned above implicitly relies on finiteness. Almost all program verfication problems involve concepts not definable in first-order logic. Methods of simulating more expressive logics in first-order logic are generally inferior in practice to systems specifically designed to go beyond first-order logic.
Higher-order systems allow quantification over predicates (i.e., concepts; Gordon 1987). Finiteness is definable in higher-order logics -- by quantifying over predicates, we can say that "finite" is the least predicate satisfying the condition given in the paragraph above. Unfortunately, because higher-order logic makes automation difficult, computer systems based on higher-order logic typically verify human-written derivations rather than attempt to find derivations automatically.
Induction systems represent a middle ground between the expressively weak first-order resolution and term-rewriting systems and the expressively strong systems based on higher-order logic (Boyer and Moore 1979). Induction systems are "first-order" in the sense that they do not typically allow quantification over predicates. But, unlike true first-order systems, all objects are assumed to be finite. A variable in a symbolic expression ranges over infinitely many different possible values, each of which is a finite object. This is different from symbolic model checking, where each variable ranges over only a finite number of possible values. Also, induction systems allow well-founded recursive definitions of the kind used in functional programming languages. The underlying logic of an induction system is best viewed as a programming language, such as cons-car-cdr Lisp. But unlike traditional implementations of a programming language, an induction system can derive symbolic equations that are true under any allowed interpretation of the variables appearing in the expressions, such as the following:
Induction systems seem most appropriate for program verification and for modeling commonsense reasoning about an arbitrary (or unknown) finite set.
Boyer, R. S., and J. S. Moore. (1979). A Computational Logic. ACM Monograph Series. Academic Press.
Burch, J. R., E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. (1990). Symbolic model checking: 10 20 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press.
Davis, M. (1983). The prehistory and early history of automated deduction. In J. Seikmann and G. Wrightson, Eds., Automation of Reasoning, vol. 1. Springer.
Fitting, M. (1996). First-Order Logic and Automated Theorem Proving. 2nd ed. Springer.
Gordon, M. (1987). Hol: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, Eds., VLSI Specification, Verification, and Synthesis. Kluwer.
McAllester, D. (1991). Some observations on cognitive judgments. In AAAI-91 Kaufmann, pp. 910-915.
Wolfram, S. (1996). Mathematica. 3rd ed. Wolfram Media and Cambridge University Press.
Copyright © 1999 Massachusetts Institute of Technology