The Logic Behind Prolog: Horn Clauses and AI Design

This article explores the foundational decisions made by Alain Colmerauer and Robert Kowalski in the early 1970s when designing the Prolog programming language. By centering the language on Horn clauses and resolution theorem proving, they bridged the gap between mathematical logic and practical computation. Their goal was to create a tool capable of handling the complex demands of artificial intelligence, specifically natural language processing and automated reasoning. Ultimately, this design choice allowed computers to process knowledge declaratively while maintaining the execution speed needed for real-world AI applications.

The Need for a Declarative AI Language In the early days of artificial intelligence, researchers struggled to represent human knowledge and language using traditional, procedural programming languages. Procedural languages required programmers to specify exact step-by-step instructions to solve a problem.

Alain Colmerauer, working on natural language translation in Marseille, and Robert Kowalski, researching automated theorem proving in Edinburgh, wanted a different approach. They envisioned a declarative paradigm. In a declarative system, the programmer only needs to state what is true (facts and rules) and what needs to be found (the goal), leaving the computer to figure out how to find the answer. Mathematical logic was the ideal framework for this, as it naturally represents relationships and truths.

Why Resolution Theorem Proving? To make logic executable by a machine, Prolog needed an inference engine—a mechanism to derive new truths from known facts. Kowalski and Colmerauer utilized a concept introduced by Alan Robinson in 1965 called the resolution principle.

Resolution theorem proving works by proof by contradiction. When a user asks a Prolog program a question, the system temporarily assumes the opposite of the question is true. It then combines this assumption with the known facts and rules in its database. If this combination leads to a logical contradiction (an empty clause), the system successfully proves that the original question must be true. This provided a unified, single rule of inference, drastically simplifying how the computer searches for answers compared to older logical systems that required dozens of different inference rules.

The Efficiency of Horn Clauses While resolution theorem proving on full first-order logic is powerful, it is computationally explosive. Full logic allows for ambiguous statements (e.g., "Either A is true, or B is true"), which forces a computer to branch out and test massive combinations of possibilities, quickly exhausting memory and processing power.

To solve this, Kowalski and Colmerauer restricted Prolog to a specific subset of logic known as Horn clauses. A Horn clause is a logical statement with at most one positive conclusion. This restriction removes ambiguity and converts logic into a predictable "if-then" structure: Conclusion A is true IF conditions B, C, and D are true.

Designing Prolog around Horn clauses solved two major problems for AI development:

1. Procedural Interpretation of Logic: Kowalski realized that a Horn clause could be read in two ways. Logically, it is an implication. Procedurally, it acts just like a subroutine in traditional programming: the conclusion is the procedure's name, and the conditions are the body of the procedure (sub-goals to be executed). This directly connected pure logic to practical computer execution.
2. Computational Speed (SLD Resolution): Restricting the language to Horn clauses allowed the use of a highly efficient variation of resolution called SLD (Selected Literal Definite) resolution. Instead of searching blindly in all directions, the computer could use backward-chaining—starting from the goal and working backward through the rules in a linear, predictable tree search.

The Impact on Artificial Intelligence By combining Horn clauses with resolution theorem proving, Colmerauer and Kowalski gave AI researchers a tool with built-in pattern matching (unification) and automatic search (backtracking). If a path of reasoning failed, Prolog would automatically backtrack and try another rule. This made Prolog uniquely suited for parsing human grammar, building expert systems, and solving complex scheduling problems, cementing its legacy as a cornerstone of symbolic artificial intelligence.