Logic Programming Overview

Logic Programming Overview

Section 1.10 of The Art of Prolog contains a summary of basic logic programming terminology, which I've reproduced with some modifications below. The most difficult part about learning Prolog is adapting to the logic programming paradigm, because the model of computation is so unusual. The chief merit of the summary is that it brings together the different pieces of the paradigm into a coherent overview. Note that implication is written using the standard symbol rather than :-/2, as in Prolog. A good reference for basic terminology in the context of SWI-Prolog is The Prolog Dictionary.

The basic structure in logic programs is the term. The set of terms consists of constants, variables and compound terms: constants denote particular individuals such as integers or atoms, while variables denote a single but unspecified individual. The symbol for an atom can be any sequence of characters (if there is a possibility of confusion with symbols for terms such as integers or variables, then the symbol is quoted). The symbol for a variable is distinguished by beginning with an uppercase letter.

A compound term consists of a functor and a sequence of one or more terms, called arguments. A functor is characterized by its name, which is an atom, and arity, or number of arguments (a functor of arity n>0 denotes a predicate). Constants are considered to be functors or arity zero. Syntactically, compound terms have the form f(t1,…,tn), where the functor has name f, arity n, and t1,…,tn are the arguments. A functor f of arity n is denoted f/n. Functors with the same name but different arities are considered distinct. A term is called ground if it contains no variables. A goal is an atom or compound term (which is generally non-ground).

A substitution is a finite set of pairs of the form X=t, where X is a variable, t is a term, and no two pairs have the same variable occurring on their left-hand sides. For any substitution θ={X1=t1,…,Xn=tn} and term s, the term sθ denotes the result of simultaneously replacing each occurrence of the variable Xi in s by the term ti for 1≤i≤n. The term sθ is called an instance of s.

A logic program is a finite set of clauses. A clause or rule is a universally quantified logical statement of the form A←B1,…,Bn, where A and each Bi are goals. The declarative meaning of the clause is "A is implied by the conjunction of the Bi." The procedural interpretation of the clause is: "To answer the query A, answer the conjunction of the queries B1 through Bn." The goal A is called the head and B1,…,Bn the body of the clause. If n=0, the clause is called a fact or unit clause and written A. The declarative meaning of a fact A is "A is true." The procedural interpretation of A is "The goal A is satisfied."

A query is a conjunction of the form A1,…,An?, where the Ai are goals and n>0. Variables in a query are understood to be existentially quantified. A computation in a logic program P attempts to find an instance of a given query that is deducible from P. A goal G is deducible from a program P if there is an instance A of G such that A←B1,…,Bn is a ground instance of a clause in P, and each Bi is deducible from P. The deduction of a goal G from an identical fact G is a special case of deducibility.

The meaning of a logic program P is a set of ground unit goals deducible from P, and inductively defined as follows. The set of ground instances of facts in P are in the meaning of P. A ground goal G is in the meaning of P if there is a ground instance G←B1,…,Bn of a rule in P such that each Bi is in the meaning of P. The meaning of P consists of all ground instances that are deducible from P according to the preceding rules.

The intended meaning M of a program is also a set of ground unit goals. A program P is correct with respect to an intended meaning M if M(P) is a subset of M, where M(P) denotes the meaning of P. It is complete with respect to M if M is a subset of M(P). A program P is thus correct and complete with respect to its intended meaning, which is the desired situation, if and only if M=M(P). Finally, we say that a ground goal G is true with respect to an intended meaning M if G∈M, and false otherwise.