View source for Logic programming

''LP''

Logic programming came into existence in the early 1970s. Its ideal is to write programs in the language of logic, thereby aiming at an immediately obvious intuitive meaning, whereas execution can be left to an interpreter.

This ideal has been realized to a great extent in the case of positive logic programming, which forms the common core of systems of logic programming. The logical language employed here is that of Horn-clause (first-order) logic. Programs can be executed by linear resolution, which is the special case of the resolution procedure that not only is capable of refuting but has computing power at the same time.

==Herbrand universa.==
Suppose that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l1101701.png" /> is a finite set of function symbols. Every symbol in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l1101702.png" /> has an arity: a non-negative integer. Assume that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l1101703.png" /> contains at least one <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l1101704.png" />-ary symbol (a constant symbol). The set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l1101705.png" /> determines a corresponding Herbrand universe <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l1101706.png" /> of closed <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l1101708.png" />-terms, which is the least set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l1101709.png" /> of formal expressions (built using the symbols from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017010.png" />, brackets, and the comma) such that if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017011.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017012.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017013.png" />-ary, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017014.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017015.png" /> constitutes the free <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017016.png" />-algebra in which a function symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017017.png" /> is interpreted as the function that assigns the value <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017018.png" /> to arguments <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017019.png" />.

Most data types can be viewed as Herbrand universa. For instance, the non-negative integers <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017020.png" /> can be identified with the terms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017021.png" /> generated from one constant symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017022.png" /> with the help of one unary function symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017023.png" />. Similarly, one can view lists, trees, etc. as generated by means of suitable function symbols.

==Horn-clause logic.==
The set of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017025.png" />-terms is generated from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017026.png" /> in the same way as is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017027.png" />, but this time allowing variable symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017028.png" /> as terms as well.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017029.png" /> be a finite set of relation symbols (with arities). An <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017031.png" />-atom is an expression of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017032.png" /> where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017033.png" /> is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017034.png" />-ary relation symbol and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017035.png" /> are terms.

A positive literal is the same as an atom. A negative literal is the negation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017036.png" /> of an atom <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017037.png" />.

A clause is a finite sequence of (positive and/or negative) literals. Logically, a clause <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017038.png" /> is identified with the disjunctive formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017039.png" />, where variables are read as if they were quantified universally.

A rule or Horn clause is a clause in which exactly one literal is positive. Finally, a (logic) program is a finite set of rules.

Note that a Horn clause like <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017040.png" /> is identified with the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017041.png" />, which in turn is logically equivalent with the implication <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017042.png" />. It is logic programming custom to write this as

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017043.png" /></td> </tr></table>

suggesting a ( "procedural" ) interpretation of rules as something to be executed ( "in order to execute A, execute B1…Bk" ).

==Meaning of programs.==
logic programming started with the observation that many operations over a Herbrand universe can be described using a program. For instance, consider the simple case of addition over the non-negative integers. This operation is determined by the following two recursion equations:

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017044.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017045.png" /></td> </tr></table>

which enable a unique evaluation of every sum of two numbers expressed in terms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017046.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017047.png" />. (E.g., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017048.png" />.) The recursion equations transform into the following program involving a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017049.png" />-ary relation symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017050.png" />:

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017051.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017052.png" /></td> </tr></table>

In what way do these rules express addition? First, they are clearly satisfied by the Herbrand model that consists of the Herbrand universe <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017053.png" /> (the free algebra over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017054.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017055.png" />) supplied with the graph of the addition operation as a meaning for the symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017056.png" />. However, there are many more relations that similarly make <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017057.png" /> into a Herbrand model of this program. Nevertheless, addition here stands out: it happens to make <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017058.png" /> into the least Herbrand model (having fewest true atoms) of this program.

The following computational completeness theorem holds: For every computable operation over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017059.png" /> one can construct a program such that in its least Herbrand model the graph of the operation occurs as meaning of one of the relation symbols.

==Execution of programs.==
The above explains that least Herbrand models can be viewed as meanings of programs and that every computable operation surfaces in such a meaning. However, programs are meant to be executed. This is where the notion of linear resolution comes in.

A substitution is a finite function that maps variables to terms. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017060.png" /> is an expression and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017061.png" /> a substitution, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017062.png" /> is the expression obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017063.png" /> by replacing every variable from the domain of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017064.png" /> occurring in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017065.png" /> by its <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017066.png" />-image.

The substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017067.png" /> unifies the expressions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017068.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017069.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017070.png" />. It is a most general unifier (mgu) of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017071.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017072.png" /> if it unifies them and for every other unifier <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017073.png" /> there exists a substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017074.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017075.png" />.

The following unification theorem holds: If two expressions have a unifier, then they have an mgu as well. Both unifiability and mgu can be determined algorithmically.

A query is a finite sequence of atoms. In particular, the empty sequence is a query. The intuitive meaning of a query is the conjunction of its atoms (variables conceived of as universally quantified). Therefore, the empty query stands for the logically true formula.

A query represents a condition to be solved. Linear resolution aims at finding such solutions.

The notation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017076.png" />, query <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017077.png" /> resolves to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017078.png" /> via mgu <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017079.png" />, is used to describe the circumstance that for some atom <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017080.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017081.png" /> and some rule <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017082.png" /> of the program under consideration:

a) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017083.png" /> is an mgu of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017084.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017085.png" />,

b) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017086.png" /> is obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017087.png" /> by replacing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017088.png" /> by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017089.png" />.

A derivation of the query <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017090.png" /> relative to a program is a finite sequence

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017091.png" /></td> </tr></table>

where every step employs a variant of a rule of the program in which all variables are fresh (i.e., not entering earlier steps).

Such a derivation is successful if its last query is empty. As an example, here is a successful derivation of the atomic query <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017092.png" /> (that  "asks"  for the sum <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017093.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017094.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017095.png" />) relative to the program of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017096.png" /> rules given earlier. Numbers are identified with suitable terms and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017097.png" /> indicates substituting <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017098.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l11017099.png" />.

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170100.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170101.png" /></td> </tr></table>

The first two steps of this derivation are executed using the second rule, whereas the last step employs the first one. Only the relevant portions of the mgu's are indicated.

Composing the three mgu's in this example results in the computed answer substitution of the derivation that sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170102.png" /> to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170103.png" />, i.e., to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170104.png" />. The derivation is nothing but a transform of the earlier computation showing that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170105.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170106.png" /> add up to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170107.png" />.

==Correspondence.==
Meanings of programs and executions (computations) correspond in the following way (cf. the example derivation), thereby witnessing the successful accomplishment of the logic programming ideal in this context.

The soundness theorem: If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170108.png" /> is the computed answer substitution of a successful derivation of the query <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170109.png" /> via a program, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170110.png" /> follows logically from that program.

The converse is almost true.

The completeness theorem: If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170111.png" /> follows logically from a program, then there exists a computed answer substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170112.png" /> of a successful derivation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170113.png" /> via that program such that for some substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170114.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170115.png" />.

(The reason that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170116.png" /> itself may not be computed is that resolution produces answers that are  "as general as possible" .)

==Prolog.==
Linear resolution is the core of the Prolog system, which was developed more or less independently from, but at the same time as, logic programming theory. Thus, logic programming can be viewed as the theoretical basis underlying Prolog. However, many divergencies exist between logic programming theory and Prolog practice.

===Occur check.===
A relatively small difference is the fact that the Prolog implementation of the mgu algorithm is incorrect. For reasons of cheapness it omits the so-called occur check. In most situations in practice, though, this incorrectness will not surface.

===Search strategy.===
At every stage in the construction of a derivation, two choices have to be made:

i) which of the atoms in the given query should be resolved;

ii) which of the rules of the program should be employed to accomplish this. (The example derivation does not illustrate these choices.)

It can be shown that the choice of i) has no influence on the final outcome. (If a successful derivation exists, one with the same computed answer substitution will be found no matter how i) is dealt with. Usual Prolog implementations always resolve left-most atoms.) However, choice of ii) is of utmost importance. Given a selection rule that handles i), all derivations for a query via a given program form a tree. The tree splits if more than one rule is applicable to the selected atom. A branch through the tree can be successful (ending at the empty query), unsuccessful (ending at a non-empty query the selected atom of which is not resolvable using any rule), or infinite. Prolog's search of this tree is  "depth-first"  (cf. also [[Depth-first search|Depth-first search]]), employing at every step the first rule in the listing of the program that is applicable to the selected (i.e., left-most) atom. At the end of an unsuccessful branch it backtracks to the last choice and tries the next rule. It goes without saying that Prolog may follow an infinite branch all the way, and, so doing, can miss a successful branch. This brings along the important question of which programs terminate on which queries.

===Negation.===
Although the logic programming model as described above is computationally complete, in many cases the need arises for more expressibility. In particular, it is sometimes desirable to allow rules <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170117.png" /> and queries <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170118.png" /> where one or more of the literals <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170119.png" /> carry a negation symbol. Prolog does offer this possibility.

A main problem is that this move destroys the logic programming ideal: the intuitive meaning of such rules is no longer evident, although several proposals (some employing [[Many-valued logic|many-valued logic]]) have tried to restore this deficiency. The second problem, that of execution, is dealt with by Prolog in a practical way. A negated atom <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170120.png" /> is resolved successfully only if the tree of derivations for the atom <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l110/l110170/l110170121.png" /> has no infinite branch and no successful derivation.

Although this way of executing negations has many useful applications, the general meaning of this way of handling negation remains problematic.

Prolog has many extra features (such as the cut, of which negation is but one application), most of which are equally cooperative in destroying the logic programming ideal described above. The problem to close the gap between logic programming theory and Prolog practice is a persistent one.

==Where to look.==
logic programming has its own periodical: the Journal of Logic Programming. A few introductory texts are [[#References|[a1]]], [[#References|[a5]]] and [[#References|[a3]]]. The problem of negation in logic programming is reviewed in [[#References|[a2]]]. One of the many texts on Prolog is [[#References|[a7]]]. The history of logic programming theory can be traced to [[#References|[a4]]]. The general notion of resolution, in particular that of most general unification, is due to [[#References|[a6]]].

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  K.R. Apt,   "Logic programming"  J. van Leeuwen (ed.) , ''Handbook of Theoretical Computer Science'' , Elsevier  (1990)  pp. 493–574</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  K.R. Apt,   R. Bol,   "Logic programming and negation: a survey"  ''J. Logic Programming'' , '''19–20'''  (1994)  pp. 9–71</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  K. Doets,   "From logic to logic programming" , MIT  (1994)</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  R.A. Kowalski,   "Predicate logic as a programming language" , ''Proceedings IFIP'74'' , North-Holland  (1974)  pp. 569–574</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  J.W. Lloyd,   "Foundations of logic programming" , Springer  (1987)  (Edition: Second, extended)</TD></TR><TR><TD valign="top">[a6]</TD> <TD valign="top">  J.A. Robinson,   "A machine-oriented logic based on the resolution principle"  ''J. ACM'' , '''12'''  (1965)  pp. 23–41</TD></TR><TR><TD valign="top">[a7]</TD> <TD valign="top">  L. Sterling,   E. Shapiro,   "The art of Prolog" , MIT  (1994)  (Edition: Second)</TD></TR></table>