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 *x*^{2}+ *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.

- CAUSAL REASONING
- DEDUCTIVE REASONING
- FORMAL SYSTEMS, PROPERTIES OF
- MENTAL MODELS
- PROBABILISTIC REASONING
- RULES AND REPRESENTATIONS

- Expert Systems [ResearchIndex; NEC Research Institute; Steve Lawrence, Kurt Bollacker, Lee Giles]
- JC Smith: Can Machines Be Made to Think Like Lawyers?
- Mechanized Reasoning
- PC AI - Expert Systems

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.