Logic and Declarative Programming
Logic and declarative programming express problems as relations, facts, and rules, leaving the search for solutions to an inference engine rather than explicit step-by-step instructions.
Definition
Logic programming is a declarative paradigm in which a program is a set of logical clauses (facts and rules), and computation proceeds by automated deduction, typically resolution with unification, to answer queries against that knowledge.
Scope
This topic covers logic programming based on Horn clauses and resolution (as in Prolog), constraint logic programming, and the broader declarative idea of specifying what should hold rather than how to compute it. It includes unification, backtracking search, the model-theoretic and proof-theoretic semantics of logic programs, and the separation of logical specification from control.
Core questions
- What does it mean to compute by proving a goal from logical clauses?
- How do unification and backtracking realize search over a relational program?
- How is the separation of logic from control made precise?
- How do constraints extend pure logic programming?
Key theories
- Resolution principle
- Robinson's resolution gives a single, machine-oriented inference rule for first-order logic, providing the deductive engine that makes logic programming computationally feasible.
- Logic plus control
- Kowalski's analysis distinguishes the logical content of a program (what is true) from its control component (how the proof is searched), framing logic programming as a way to vary control while keeping logic fixed.
- Declarative and procedural semantics of logic programs
- Lloyd formalizes the model-theoretic, fixpoint, and operational semantics of definite logic programs and proves their correspondence, grounding the meaning of logic programs.
Clinical relevance
Declarative and logic-based techniques underpin database query languages, constraint solvers, knowledge representation, and rule engines. Their emphasis on specifying problems rather than algorithms makes them well suited to combinatorial search, configuration, and reasoning tasks.
History
Robinson's 1965 resolution principle laid the deductive groundwork. In the early 1970s Colmerauer and Roussel created Prolog, and Kowalski articulated the procedural interpretation of Horn clauses. The paradigm flourished through the 1980s, influencing Japan's Fifth Generation project, and later expanded into constraint logic programming and answer-set programming.
Debates
- Purity versus practical control
- Logic programming languages balance the ideal of pure declarative logic against practical needs for explicit control, such as cut and ordering, which improve efficiency but compromise the clean logic/control separation.
Key figures
- Robert Kowalski
- Alain Colmerauer
- J. Alan Robinson
- John Lloyd
- Philippe Roussel
Related topics
Seminal works
- kowalski1979
- robinson1965
- lloyd1987
- colmerauer1993
Frequently asked questions
- How does logic programming differ from imperative programming?
- Instead of specifying a sequence of operations, a logic program declares facts and rules, and an inference engine searches for proofs that answer queries, so the programmer focuses on what is true rather than how to compute it.
- What is unification?
- Unification is the process of finding a substitution that makes two logical terms identical; it is the core mechanism by which logic programs match goals against clause heads.