Logic programming – Wikipedia

Programming paradigm based on formal logic

Logic programming is a programming, database and knowledge-representation and reasoning paradigm which is based on formal logic. A program, database or knowledge base in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic programming language families include Prolog, Answer Set Programming (ASP) and Datalog. In all of these languages, rules are written in the form of clauses:

A :- B₁, …, B_n.

and are read declaratively as logical implications:

A if B₁ and … and B_n.

A is called the head of the rule, B₁, …, B_n is called the body, and the B_i are called literals or conditions. When n = 0, the rule is called a fact and is written in the simplified form:

A.

Queries (or goals) have the same syntax as the bodies of rules and are commonly written in the form:

?- B₁, …, B_n.

In the simplest case of Horn clauses (or “definite” clauses), all of the H, B₁, …, B_n are atomic formulae of the form p(t₁ ,…, t_m), where p is a predicate symbol naming a relation, like “motherhood”, and the t_i are terms naming objects (or individuals). Terms include both constant symbols, like “charles”, and variables, such as X, which start with an upper case letter.

Consider, for example, the following Horn clause program:

mother_child(elizabeth, charles).
father_child(charles, william).
father_child(charles, harry).
parent_child(X, Y) :- 
     mother_child(X, Y).
parent_child(X, Y) :- 
     father_child(X, Y).
grandparent_child(X, Y) :- 
     parent_child(X, Z), 
     parent_child(Z, Y).

The program can be queried both to generate grandparents and to generate grandchildren. It can even be used to generate all pairs of grandchildren and grandparents:

?- grandparent_child(X, william).
X = elizabeth.

?- grandparent_child(elizabeth, Y).
Y = william
Y = harry.

?- grandparent_child(X, Y).
X = elizabeth
Y = william.
X = elizabeth
Y = harry.

Although Horn clause logic programs are Turing complete,^[1][2] for most practical applications, Horn clause programs need to be extended to “normal” logic programs with negative conditions. For example, the definition of sibling uses a negative condition, where the predicate = is defined by the clause X = X:

sibling(X, Y) :- 
     parent_child(Z, X), 
     parent_child(Z, Y), 
     not(X = Y).

Logic programming languages that include negative conditions have the knowledge representation capabilities of a non-monotonic logic.

In ASP and Datalog, logic programs have only a declarative reading, and their execution is performed by means of a proof procedure or model generator whose behaviour is not meant to be controlled by the programmer. However, in the Prolog family of languages, logic programs also have a procedural interpretation as goal-reduction procedures:

to solve A, solve B₁, and … and solve B_n.

Negative conditions in the bodies of clauses also have a procedural interpretation, known as negation as failure: A negative literal not B is deemed to hold if and only if the positive literal B fails to hold.

Much of the research in the field of logic programming has been concerned with trying to develop a logical semantics for negation as failure and with developing other semantics and other implementations for negation. These developments have been important, in turn, for supporting the development of formal methods for logic-based program verification and program transformation.

History[edit]

The use of mathematical logic to represent and execute computer programs is also a feature of the lambda calculus, developed by Alonzo Church in the 1930s. However, the first proposal to use the clausal form of logic for representing computer programs was made by Cordell Green.^[3] This used an axiomatization of a subset of LISP, together with a representation of an input-output relation, to compute the relation by simulating the execution of the program in LISP. Foster and Elcock’s Absys, on the other hand, employed a combination of equations and lambda calculus in an assertional programming language that places no constraints on the order in which operations are performed.^[4]

Logic programming, with its current syntax of facts and rules, can be traced back to debates in the late 1960s and early 1970s about declarative versus procedural representations of knowledge in artificial intelligence. Advocates of declarative representations were notably working at Stanford, associated with John McCarthy, Bertram Raphael and Cordell Green, and in Edinburgh, with John Alan Robinson (an academic visitor from Syracuse University), Pat Hayes, and Robert Kowalski. Advocates of procedural representations were mainly centered at MIT, under the leadership of Marvin Minsky and Seymour Papert.^[5]

Although it was based on the proof methods of logic, Planner, developed by Carl Hewitt at MIT, was the first language to emerge within this proceduralist paradigm.^[6] Planner…