Logic programming

Logic programming is a programming paradigm in which computation is expressed through sentences of formal logic. A logic program describes relations among terms, while an associated inference mechanism derives consequences of those relations or searches for substitutions that satisfy a query. Most established logic programming systems are based on restricted forms of first-order logic, particularly Horn clauses, because these forms admit systematic proof procedures with direct computational interpretations.

The paradigm combines a declarative reading, under which a program specifies which propositions follow from its clauses, with an operational reading determined by a particular resolution strategy. This combination distinguishes logic programming from both unrestricted automated theorem proving and conventional programming organized primarily around explicit sequences of state-changing operations.

Logical foundations

A conventional logic program consists of clauses having the form

H :- B1, B2, ..., Bn.

Here, H is the head of the clause, while the expressions following the implication symbol constitute its body. Under the declarative interpretation, the clause states that H holds whenever every body formula holds. A clause with an empty body represents a fact, whereas a query is treated as a goal whose logical consequences and variable substitutions are to be determined.

For example, a relation describing ancestry can be represented by clauses equivalent to the following:

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

The first clause states that parenthood entails ancestry. The second gives ancestry a recursive structure by relating an ancestor to an intermediate parent. A query such as ancestor(a, Y) asks for substitutions for Y that are supported by the program and its inference rules.

The dominant operational mechanism in classical logic programming is SLD resolution, a specialization of resolution for definite clauses. During an SLD derivation, a selected goal is matched against the head of a program clause. The matching process uses unification to compute a substitution under which the expressions agree, after which the selected goal is replaced by the instantiated body of the clause. A successful derivation ends with no remaining goals and yields a computed answer substitution.

The declarative semantics of definite programs is commonly formulated through Herbrand interpretations. Each program has a least Herbrand model containing exactly the ground atomic consequences generated by its clauses. The same meaning can be characterized as the least fixed point of the program’s immediate-consequence operator. Robert Kowalski and Maarten van Emden established the correspondence between these model-theoretic and fixed-point accounts, providing a semantic basis for relating logical consequence to program execution.

Historical development

The intellectual basis of logic programming emerged from twentieth-century work on symbolic logic, mechanical proof, and computational linguistics. Resolution, introduced by John Alan Robinson in 1965, supplied a general inference rule for first-order theorem proving. Research during the following decade restricted and reorganized resolution so that logical formulas could function as executable program clauses rather than solely as inputs to a general theorem prover.

The first Prolog system was developed at the University of Aix-Marseille in the early 1970s. Alain Colmerauer and Philippe Roussel formulated the language in connection with natural-language processing, while Robert Kowalski’s procedural interpretation of Horn clauses supplied part of its theoretical organization. In 1973, Gérard Battani, Henri Meloni, and You Watanabe implemented components of the Marseille system in Fortran, including term representation, unification, and the management of alternative clause choices. Their implementation contributed to the transition from experimental resolution programs to a recognizable programming-language system.

Early Prolog adopted a depth-first, left-to-right search discipline. This execution rule reduced the amount of control information required by the runtime system, but it also made termination dependent on clause order and goal order. The resulting language therefore did not identify operational behavior entirely with logical meaning: two programs with the same declarative consequences could exhibit different execution times, enumerate answers in different orders, or fail to terminate under the same query.

During the later 1970s, David H. D. Warren developed an influential Prolog compiler for the DECsystem-10. His subsequent abstract-machine design, known as the Warren Abstract Machine, represented logic variables, environments, choice points, and backtracking through a compact instruction architecture. These techniques became a common implementation basis for later Prolog systems and clarified how unification-based execution could be compiled rather than interpreted directly.

Logic programming also became associated with the Japanese Fifth Generation Computer Systems project during the 1980s. That project used logic-based languages as a foundation for parallel symbolic computation and knowledge processing. Its principal language, Concurrent Prolog and related committed-choice systems, altered conventional Prolog execution by replacing unrestricted backtracking with synchronization and commitment mechanisms suited to concurrent processes.

Operational semantics and control

In pure definite-clause logic programming, the logical content of a program is independent of the order in which clauses are written. Concrete systems nevertheless require a selection rule for choosing the next goal and a search rule for examining applicable clauses. Prolog conventionally selects the leftmost goal and considers clauses in textual order, backtracking to earlier choice points when a later subgoal fails.

This search model gives clause order an operational role not represented in the least-model semantics. A recursive clause placed before a terminating base clause can generate an infinite derivation even when a finite proof exists. Similarly, depth-first search can remain indefinitely within one branch of a proof tree and never reach a successful branch located elsewhere. These effects arise from the incompleteness of the search strategy rather than from the resolution rule itself.

Many Prolog systems include the cut operator, written !, which discards selected alternatives created since entry into the current predicate. Cut changes the reachable search space and can therefore affect the set of computed answers. Programs using it are interpreted partly through Prolog’s operational semantics rather than entirely through ordinary logical implication.

Negation presents a related distinction. Classical first-order negation does not generally provide an effective execution rule for open-world logic programs, so Prolog commonly implements negation as failure. Under this rule, a ground goal is treated as false when an attempted proof finitely fails. Its semantic analysis is connected with Clark's completion, stratified programs, and several forms of non-monotonic logic. The result differs from classical negation because failure to derive a proposition becomes computationally significant.

Constraints and restricted languages

Constraint logic programming extends the Horn-clause framework by interpreting selected predicates within a specialized constraint domain. Instead of enumerating every value through ordinary unification, a constraint solver maintains conditions over variables and determines whether their conjunction remains satisfiable. Different systems support domains based on real arithmetic, finite integer sets, or linear rational relations, with each domain supplying its own consistency and propagation operations.

This extension modifies the meaning of an intermediate computational state. A variable can remain associated with a set of admissible values rather than receiving a single ground term immediately, and a successful derivation can return residual constraints as part of its answer. The logical reading remains relational, while the operational machinery combines resolution with domain-specific decision procedures.

Datalog imposes a different restriction by excluding general function symbols and commonly requiring range-restricted rules. For finite input databases, these conditions produce a finite space of ground facts and support bottom-up fixed-point evaluation. Datalog consequently occupies an intersection between logic programming and relational database theory, where recursive rules express relations such as transitive closure while query optimizations avoid repeatedly deriving identical facts.

Tabled logic programming introduces memoization at the level of subgoals and their answers. When a previously encountered call recurs, evaluation reuses or extends a table instead of entering an independent depth-first derivation. Under suitable conditions, tabling prevents several common forms of infinite recursion and implements fixed-point computations compatible with the semantics of recursive rules. SLG resolution generalizes this approach to programs containing negation and supports the well-founded semantics.

Relationship between programs and proofs

A successful logic-program execution can be interpreted as the construction of a proof. Clause selection corresponds to the use of an implication, while unification identifies the substitution required to apply that implication. This interpretation connects logic programming with the broader correspondence between computation and formal deduction, although ordinary Prolog permits extra-logical operations whose behavior is not reducible to proof search.

The slogan “algorithm equals logic plus control,” associated with Kowalski’s account of the paradigm, separates the logical relations expressed by clauses from the strategy governing their use. In implemented languages, the separation is partial rather than absolute. Search order affects termination and resource consumption, while arithmetic evaluation, input and output, dynamic clause modification, and term inspection introduce behavior beyond a program’s least logical model.

Modern logic programming consequently comprises several related semantic traditions rather than one uniform execution model. Classical Prolog emphasizes ordered SLD resolution and backtracking. Datalog emphasizes finite fixed-point evaluation over relational structures, while constraint systems integrate proof search with specialized theories. Answer-set programming uses stable-model semantics to compute models of non-monotonic rule sets and is generally classified as a neighboring form of declarative programming rather than as a direct variant of Prolog execution.

See also

  • Declarative programming, the broader classification of programs organized around specifications of results and relations.
  • Functional programming, a paradigm whose formal basis is associated primarily with function application and the lambda calculus.
  • Answer set programming, a rule-based formalism using stable-model semantics for non-monotonic inference.
  • Inductive logic programming, a field that derives logical hypotheses from examples and background knowledge.
  • Automated reasoning, the study of computational methods for deriving consequences within formal systems.
  • Deductive database, a database system in which logical rules supplement stored relations.
  • Term rewriting, a computational framework based on the repeated transformation of symbolic expressions.
  • Type theory, a family of formal systems connecting logical propositions with structured computational objects.