Logic: Can a machine reason?

In the seventeenth century Leibniz dreamed of a calculus ratiocinator: a language so precise that disputes could be settled by calculating. “Let us calculate”, two philosophers would say, and sit down with pencil and paper. Two centuries later George Boole wrote the laws of thought as algebra (The Laws of Thought, 1854), and in 1879 Gottlob Frege published the Begriffsschrift, the first complete formal language for mathematics: variables, quantifiers and rules of inference.

When computers arrived, the dream looked within reach. If reasoning is calculating, and a computer calculates, then a computer can reason. In 1956, at the same Dartmouth workshop that named the field, Allen Newell, Herbert Simon and Cliff Shaw presented the Logic Theorist, which proved 38 of the first 52 theorems in chapter 2 of Russell and Whitehead's Principia Mathematica. Symbolic AI was born: intelligence as the manipulation of symbols according to logical rules.

Truth and proof

First-order logic talks about objects ( $x$ , $y$ , $tom$ ), functions ( $father (x)$ ), relations ( $parent (x, y)$ ), connectives ( $\neg, \land, \lor, \to$ ) and the quantifiers $\forall$ and $\exists$ . A set of formulas $Γ$ can say, for example, that every parent of an ancestor is an ancestor:

\forall x \forall y \forall z (parent (x, z) \land anc (z, y) \to anc (x, y)) .

There are two ways of saying that a formula $φ$ “follows” from $Γ$ . The semantic one, $Γ ⊨ φ$ : $φ$ is true in every world (every interpretation of the symbols) in which all of $Γ$ is true. And the syntactic one, $Γ ⊢ φ$ : there is a proof, a finite sequence of formulas in which each step applies a mechanical rule. The first is about meaning, the second about pushing symbols around. The miracle is that they coincide.

Theorem (completeness, Gödel 1929)

For every set of first-order formulas $Γ$ and every formula $φ$ ,

Γ ⊨ φ ⟺ Γ ⊢ φ .

Every truth that follows from the axioms has a proof, and every proof establishes a truth. This is what makes the Leibniz dream plausible: “true in all worlds”, an infinite notion, is reduced to “there is a finite proof”, which a machine can search for. Do not confuse it with Gödel's other, more famous theorem: incompleteness (1931) says that no consistent, effective set of axioms proves every truth about the natural numbers. Completeness is about what follows from the axioms; incompleteness, about what the axioms fail to pin down.

But searching is not deciding. Proofs can be listed one by one, so if $Γ ⊢ φ$ the search will eventually find a proof. If $φ$ does not follow, the search may never end. In 1936 Church and Turing proved that this cannot be fixed: there is no algorithm that decides whether a first-order formula is valid. It is the logical face of the halting problem. First-order logic is semi-decidable: a machine can confirm every consequence, but it cannot always rule one out.

Resolution: one rule is enough

Proof systems for humans have many rules. In 1965 John Alan Robinson found one that is enough by itself, and is made for machines. First, every formula is turned into clausal form: a conjunction of clauses, each a disjunction of literals (atoms or negated atoms), with the existential quantifiers replaced by new functions (Skolem functions) and the universal ones left implicit. Satisfiability is preserved, and that is enough, because to prove $φ$ from $Γ$ it suffices to show that $Γ \cup {\neg φ}$ has no model.

Definition (resolution rule)

From two clauses with complementary literals $L$ and $\neg L^{'}$ that can be made equal by a substitution $θ$ , derive their resolvent:

\frac{C \lor L D \lor \neg L^{'}}{(C \lor D) θ} θ = mgu (L, L^{'}) .

Theorem (soundness and refutation completeness of resolution, Robinson 1965)

A set of clauses $S$ is unsatisfiable if and only if the empty clause $□$ can be derived from $S$ by resolution.

Deriving $□$ means having reached a contradiction, as in a proof by reductio ad absurdum. Behind the theorem lies Herbrand's (1930): a set of clauses is unsatisfiable if and only if some finite set of its ground instances (with constants substituted for the variables) already is, as plain propositional logic. Resolution searches for those instances lazily, substituting only what is needed. The key to doing that is the operation in the rule's subscript, which deserves a section of its own.

Unification

To resolve $parent (tom, X)$ against $\neg parent (Y, bob)$ we need a substitution that makes both atoms equal: $θ = {X \mapsto bob, Y \mapsto tom}$ . A substitution like that is a unifier. There can be infinitely many (to unify $f (X)$ and $f (Y)$ you can set both to $a$ , to $b$ , to $g (a)$ …), but they are not all equally good: ${X \mapsto Y}$ commits to nothing more than it has to.

Theorem (most general unifier, Robinson 1965)

If two terms $s$ and $t$ have a unifier, they have a most general one, $θ = mgu (s, t)$ : every unifier $σ$ of $s$ and $t$ can be written as $σ = θ λ$ for some substitution $λ$ . It is unique up to renaming variables, and there is an algorithm that computes it or reports that it does not exist.

Proof (the Martelli–Montanari algorithm)

Start from the set of equations ${s = t}$ and apply any of these rules while one applies:

Decompose: replace $f (s_{1}, \dots, s_{n}) = f (t_{1}, \dots, t_{n})$ by $s_{1} = t_{1}, \dots, s_{n} = t_{n}$ .
Clash: if $f (\dots) = g (\dots)$ with different symbols or arities, fail.
Delete: remove $X = X$ .
Swap: replace $t = X$ , with $t$ not a variable, by $X = t$ .
Occurs check: if $X = t$ with $X$ occurring inside $t \neq X$ , fail.
Eliminate: if $X = t$ with $X$ not in $t$ but present in other equations, substitute $t$ for $X$ in all of them.

Each rule preserves the set of unifiers of the system, and the two failure rules apply only to systems without unifiers: no substitution makes $f$ equal to $g$ , and none makes $X$ equal to a term strictly larger than itself. The process terminates, because each step reduces, in lexicographic order, the number of variables not yet solved, the total size of the terms and the number of equations of the form $t = X$ . When no rule applies, the system has the form ${X_{1} = t_{1}, \dots, X_{k} = t_{k}}$ , with distinct variables that appear nowhere else. Then $θ = {X_{i} \mapsto t_{i}}$ is a unifier, and since the original system has the same unifiers as the final one, any other unifier $σ$ must satisfy $X_{i} σ = t_{i} σ$ , that is, $σ = θ σ$ . So $σ$ factors through $θ$ .

The unification algorithm, rule by rule. Write two terms (variables start with a capital letter) or choose an example. The last two examples fail: one because of a clash of symbols, the other because of the occurs check, which would require

X

to equal

f (X)

, an infinite term.

Prolog: logic as a program

Resolution on arbitrary clauses explodes combinatorially. But if every clause has at most one positive literal (a Horn clause), it can be read as a rule, “ $A$ is true if $B_{1}, \dots, B_{n}$ are”:

A \leftarrow B_{1} \land \dots \land B_{n} .

In 1972 Alain Colmerauer and Philippe Roussel, in Marseille, built a language on that idea to process natural language: Prolog (programmation en logique). Robert Kowalski, in Edinburgh, gave the theory: a set of Horn clauses can be read in two ways, as statements that are true or as procedures that are executed. He summed it up as “algorithm = logic + control”. You write what is true; the machine decides how to search.

parent(tom, bob).        % facts: clauses with no body
parent(bob, ann).
parent(bob, pat).

anc(X, Y) :- parent(X, Y).              % rules: ":-" reads "if"
anc(X, Y) :- parent(X, Z), anc(Z, Y).   % "," reads "and"

A query such as ?- anc(tom, Who). is a goal to refute: the machine assumes that nobody is a descendant of Tom and looks for the contradiction. Resolving always the leftmost goal against the program's clauses, in order, is SLD resolution, and the substitution it collects along the way is the answer: Who = bob, Who = ann, Who = pat.

What a logic program means

A program has a meaning independent of how it is run. Call $ℬ_{P}$ the set of all ground atoms (atoms without variables) that can be written with the program's symbols, and $ground (P)$ the set of ground instances of its clauses. Consider the operator that takes a set $I \subseteq ℬ_{P}$ and returns everything that can be deduced from it in one step:

T_{P} (I) = {A : (A \leftarrow B_{1}, \dots, B_{n}) \in ground (P), B_{1}, \dots, B_{n} \in I} .

Theorem (least Herbrand model, van Emden and Kowalski 1976)

Every definite program $P$ has a least model $M_{P}$ . It is the least fixed point of $T_{P}$ , it is reached by iterating from the empty set, and it contains exactly the ground atoms that follow from $P$ :

M_{P} = ⋃_{k \geq 0} T_{P}^{k} (\emptyset) = {A \in ℬ_{P} : P ⊨ A} .

Proof

A set of ground atoms $I$ is a model of $P$ exactly when $T_{P} (I) \subseteq I$ : every rule whose body holds in $I$ has its head in $I$ . The intersection of models is a model (if the body is in all of them, so is the head), so there is a least model, $M_{P}$ , the intersection of all of them.

$T_{P}$ is monotone ( $I \subseteq J$ implies $T_{P} (I) \subseteq T_{P} (J)$ ) and, since each body is finite, continuous: an atom deduced from a union of an increasing chain is already deduced at some finite stage. By Kleene's fixed-point theorem, $⋃_{k} T_{P}^{k} (\emptyset)$ is the least fixed point. It is contained in every model, by induction on $k$ , and is itself a model, so it equals $M_{P}$ . Finally, $P ⊨ A$ for a ground $A$ means that $A$ is true in every model of $P$ , and it is enough to look at models made of ground atoms (any model induces one with the same true ground atoms). If $A$ is true in all of them it is in $M_{P}$ ; and every atom of $M_{P}$ is true in all of them, because they all contain $M_{P}$ .

For the family program: $T_{P} (\emptyset)$ contains the three facts; one more step adds $anc (tom, bob)$ , $anc (bob, ann)$ and $anc (bob, pat)$ ; one more, $anc (tom, ann)$ and $anc (tom, pat)$ ; and after that nothing new appears. That is the meaning of the program, and the procedure matches it:

Theorem (soundness and completeness of SLD resolution)

Let $P$ be a definite program and $G$ a query. Every answer computed by SLD resolution is correct ( $P$ implies the instantiated query), and for every correct answer there is a computed answer that is at least as general, provided the tree of possibilities is explored fairly.

The proviso matters. Prolog explores the tree depth first, clause by clause, because it is fast and uses little memory. But if a branch is infinite, Prolog falls into it and never comes back, even though there are answers further to the right. Write the recursive rule as anc(X, Y) :- anc(Z, Y), parent(X, Z). and put it first: the logical meaning is exactly the same, but the program no longer answers anything. Compare both versions in the figure.

The SLD tree of a query, explored in Prolog's order: depth first, top to bottom. Each row is a list of pending goals; the label says which clause was used and what was substituted. □ is a success (an answer) and ✗ a dead end. With left recursion the first branch is infinite and Prolog never gets past it.

Prolog also adds pieces from outside pure logic: arithmetic (X is Y + 1), the cut !, which prunes alternatives in the tree, and negation as failure (Clark, 1978): \+ P succeeds if $P$ cannot be proved. It is the closed-world assumption, “what I cannot deduce is false”. It is very practical in databases, and not monotonic: adding a fact can turn a conclusion false.

Your own Prolog

The figure below is a complete Prolog interpreter running in your browser: unification, backtracking, cut, arithmetic with integers of any size, lists, definite clause grammars and the usual built-in predicates. Choose an example, edit it or write your own program, and ask it questions. Turn on the trace to see the four classic ports of each call: Call, Exit, Redo and Fail.

A Prolog interpreter in the browser, with no server: the program is loaded when you press “Consult”, and each query shows its answers one at a time, as in a real Prolog. There is a limit on inference steps, so an infinite loop ends with an error instead of freezing the page.

Expert systems, and their limits

In the 1970s and 1980s symbolic AI went to industry. Expert systems stored the knowledge of a specialist as hundreds or thousands of rules: MYCIN (Stanford, 1976) recommended treatments for blood infections, and in a 1979 blind evaluation its prescriptions were rated as highly as those of infectious-disease specialists; XCON configured DEC computers and saved the company millions a year. In 1982 Japan launched the Fifth Generation Computer Systems project, ten years of public money to build machines that would run logic programs in parallel. Logic programming was its core.

It did not deliver what it promised. The obstacles were not in the logic but in the world:

The knowledge acquisition bottleneck. Experts know more than they can put into rules, and every rule has exceptions to the exceptions.
Brittleness. Outside the cases foreseen by the rules, an expert system does not degrade gracefully: it simply fails.
Uncertainty. Logic speaks of true and false, and the world is made of “probably”. MYCIN had to invent ad hoc “certainty factors”.
The combinatorial explosion. Semi-decidability and the size of the search space are not technicalities: they make reasoning expensive exactly where it matters.

The Lisp machine market collapsed in 1987, and with it came the second AI winter. But logic did not disappear. It lives on in Datalog and in the recursive queries of SQL, in type inference, in SAT and SMT solvers that verify chips and programs, in theorem provers like Lean, which mathematicians now use to check proofs, and in systems that combine language models with symbolic tools. The difference from that era is the order: today the rules are not written by hand, they are learned.

Learning from examples means accepting that conclusions are never certain, only more or less likely. Reasoning with degrees of belief instead of with truth values requires another mathematics. That is probability.

References

G. Boole (1854). An Investigation of the Laws of Thought. Walton and Maberly.
G. Frege (1879). Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle.
K. Gödel (1930). “Die Vollständigkeit der Axiome des logischen Funktionenkalküls”. Monatshefte für Mathematik und Physik, 37.
A. Newell and H. A. Simon (1956). “The Logic Theory Machine”. IRE Transactions on Information Theory, 2(3).
J. A. Robinson (1965). “A Machine-Oriented Logic Based on the Resolution Principle”. Journal of the ACM, 12(1).
R. Kowalski (1974). “Predicate Logic as Programming Language”. Proceedings of IFIP Congress 74.
M. H. van Emden and R. Kowalski (1976). “The Semantics of Predicate Logic as a Programming Language”. Journal of the ACM, 23(4).
K. L. Clark (1978). “Negation as Failure”. In Logic and Data Bases, Plenum Press.
A. Martelli and U. Montanari (1982). “An Efficient Unification Algorithm”. ACM Transactions on Programming Languages and Systems, 4(2).
J. W. Lloyd (1987). Foundations of Logic Programming, 2nd ed. Springer.
A. Colmerauer and P. Roussel (1993). “The Birth of Prolog”. ACM SIGPLAN Notices, 28(3).

§Truth and proof

§Resolution: one rule is enough

§Unification

§Prolog: logic as a program

§What a logic program means

§Your own Prolog

§Expert systems, and their limits

§References