Logic Programming: Clauses as Programs

A theorem prover usually starts with a statement and searches for a derivation. A logic program can start with an open query and search for substitutions that make the query follow from its clauses.

The resulting proof search computes an answer. This connects deduction with programming while making the choice of search strategy especially visible.

The emergence of Prolog

Robert Kowalski developed a procedural interpretation of logical clauses, drawing on resolution and work with Donald Kuehner on linear resolution. His 1974 paper “Predicate Logic as Programming Language” presented the approach systematically.

Alain Colmerauer, Philippe Roussel, and their collaborators in Marseille developed Prolog in the early 1970s, with natural-language processing playing an important role in its origins.

The interaction between theoretical interpretation and implementation is central to this history. Prolog did not emerge from a purely abstract theorem followed by an automatic translation into software.

Colmerauer and Roussel's first-person history distinguishes preliminary work in 1971 from the more developed system of 1972 and subsequent refinement.

Kowalski's later formulation “algorithm = logic + control” captures the distinction we will examine: clauses describe relationships, while control determines how their consequences are explored.

Horn clauses as rules

A definite Horn clause has one positive head and a conjunction of positive atoms in its body:

Its variables are universally quantified. Operationally, it can be read: to establish $H$, establish each $B_i$ with compatible substitutions.

In conventional Prolog notation, the direction is written as a head followed by its conditions:

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

The notation does not make the relationship into an ordinary assignment statement. It describes a relation that can support different queries.

A query with computed answers

Add two facts:

parent(ada, ben).
parent(ben, cara).

Ask:

?- ancestor(ada, Who).

Using the first ancestor clause reduces the goal to finding a fact of the form parent(ada, Who). Unification with the first fact gives the answer Who = ben.

On backtracking, the recursive clause can be tried. It introduces an intermediate person Z and the goals parent(ada, Z) and ancestor(Z, Who).

The parent fact sets Z = ben. The remaining ancestor goal can then use the direct clause and the second parent fact, producing Who = cara.

Each answer arises from a proof of a corresponding ground instance. The variable assignments accumulated along the derivation form the computed substitution.

SLD resolution

SLD resolution specializes linear resolution to definite clauses with a selected goal atom.

At each step, the procedure selects an atom from the current goal, chooses a program clause whose head unifies with it, and replaces the atom with the clause's body under the resulting substitution.

Variables in reused clauses must be renamed freshly to prevent unrelated uses from accidentally sharing variables.

For definite programs, appropriate completeness results connect successful derivations with logical consequences. Those results do not imply that every practical traversal of the search tree will discover every answer.

Ordinary Prolog execution usually selects goals from left to right and explores alternatives depth first in clause order. This is efficient and predictable for many programs, but it can remain on an infinite branch while a successful branch exists elsewhere.

The same consequence, a different execution

Consider this program:

p(X) :- p(X).
p(a).

The fact p(a) makes p(a) a logical consequence. The first clause adds a logically redundant implication.

Under ordinary depth-first execution with the recursive clause first, a query for p(a) repeatedly selects the same recursive clause. It never reaches the fact.

Moving the fact before the recursive clause yields an immediate first answer. Reordering clauses has not changed the set of logical consequences, but it has changed what the execution produces before diverging.

Tabling can address important classes of repeated subgoals by storing and reusing answers. Breadth-first or other fairer searches make different tradeoffs. Logic programming therefore contains an ongoing study of control, not a promise that control disappears.

Negation and the closed world

Negation as failure treats a goal as unsuccessful when a search for its positive form finitely fails under the relevant execution conditions.

That is different from deriving classical negation. If a database contains no record that a person is enrolled, the absence can support “not enrolled” only under an additional interpretation that the database is sufficiently complete for that question.

With variables, the distinction becomes sharper. Testing whether any instance of a goal succeeds is not the same operation as enumerating all objects for which its classical negation holds.

Keith Clark's work on negation as failure and later semantic accounts helped formalize such issues. Stratification, well-founded semantics, and stable-model semantics provide different treatments in richer languages.

These developments should be introduced with their assumptions. There is no single interpretation that turns every operational use of failure into ordinary classical negation.

Cut, unification, and implementation choices

Prolog's cut prunes alternatives in the search. Used carefully, it can remove redundant work; used differently, it can change which answers are returned.

A program containing cut therefore needs an account of its control behavior in addition to a reading of its pure clauses.

The occurs check is another boundary. Standard finite-term unification rejects a proposed equation such as X = f(X). Some implementations omit the check for efficiency or support rational-tree terms intentionally.

Neither choice should be silently presented as exactly the finite first-order term calculus in the resolution note.

David H. D. Warren's work on efficient Prolog implementation, including the Warren Abstract Machine, helped make logic programming practical. That implementation history belongs alongside the logical principles because memory organization and execution costs shaped the usable language.

Declarative and fixed-point semantics

Maarten van Emden and Kowalski's 1976 work connected operational, model-theoretic, and fixed-point accounts of definite programs.

Begin with the program's facts. Repeatedly add every head whose body is already established. The least fixed point of this immediate-consequence operation gives the least Herbrand model in the standard setting.

For the ancestor example, the parent facts first support direct ancestors. Further iterations add longer chains.

This describes the meaning independently of a particular depth-first traversal. The separation lets us ask whether an implementation computes the intended relation and how much of that relation it actually enumerates.

Datalog and constraints

Datalog restricts the basic setting to function-free rules over a finite database, with suitable safety conditions. The resulting finite collection of possible ground atoms supports terminating fixed-point evaluation for positive programs.

This makes recursive relations useful in databases and program analysis. Termination comes from the restrictions and finite setting, not from logic programming in complete generality.

Constraint logic programming extends answer substitutions with constraints in a chosen domain. Joxan Jaffar and Jean-Louis Lassez's work in the 1980s provided a general framework, alongside related developments such as Colmerauer's constraint-oriented Prolog systems.

An answer may then specify a relationship such as $x+y=10$ with $x\ge0$, rather than enumerate every numerical pair immediately. Constraint solving cooperates with logical search, but the permitted domain and solver determine the guarantees.

From generated answers to checked mathematics

Logic programming shows how proof search can become execution. Proof assistants pursue a complementary aim: support human-directed mathematical development while controlling the rules by which a theorem is accepted.

Sources and further reading

• Robert Kowalski, “Predicate Logic as Programming Language” (1974); “Algorithm = Logic + Control” (1979).
• Maarten H. van Emden and Robert A. Kowalski, “The Semantics of Predicate Logic as a Programming Language” (1976).
• Keith L. Clark, “Negation as Failure” (1978).
• David H. D. Warren, An Abstract Prolog Instruction Set (1983).
• Joxan Jaffar and Jean-Louis Lassez, “Constraint Logic Programming” (1987).
• Alain Colmerauer and Philippe Roussel, “The Birth of Prolog”, 1992 manuscript, presented at HOPL in 1993.