LOGIC PROGRAMMING

A declarative programming
"Top-down inference unifies problem solving and computer programming" (Robert Kowalski).

---

The Theory of Logic Programming and the Prolog Language
Logic Programming

The main idea of logic programming is the separation of the logic and the execution mechanism (control), informally expressed by Robert Kowalski [1979] by means of

Algorithm = Logic + Control

Logic specifies the "what". Control specifies the "how".

The intended purpose of this separation is that the programmer specifies what is known (the logical relationships) and that it is the system that automatically responds to possible queries posed to the Knowledge Base.

In traditional imperative languages:

• The style is imperative or procedural.
  
  
• The logic is not clearly defined.
  
  
• Control is explicit.
  
  
• Both (logic and control) are mixed.
  
  
• The order of the sentences is a decisive aspect.
  
  
• A clear distinction is made between data and results.
  
  
• Logical inferences are not automatic. They must be programmed on a case-by-case basis.

On the other hand, in logic programming-oriented languages, the situation is the opposite:

• The style is declarative. Only what we know is coded: the facts and the rules, without us having to consider the type of process to be performed.
  
  
• The logic is perfectly defined.
  
  
• Control is not explicit, but underlying.
  
  
• Both (logic and control) are separate.
  
  
• The order of logic statements, in principle, can be any.
  
  
• What is data and what is result is not defined a priori.
  
  
• Inferences are automatic.

Clausal logic

Logic programming is based on clausal logic, which is a restriction of first-order predicate logic in which the logical expressions (clauses) are of conditional type and have the following form: the antecedent is of n terms connected by the logical operator "and" and the consequent consists of only one term. These are the so-called "Horn clauses" [1951], after Alfred Horn, who studied them, and they have the form

h ← c1, c2, ... , cn

The expression h is called the "header" of the clause. The set of expressions ci is called the "body" of the clause and are the necessary conditions for the consequent to be verified. The commas between the conditions are interpreted as logical "and".

In Horn clauses there are no explicit quantifiers. Free variables are considered to be universally quantified.

There can be several Horn clauses with the same header. This means that the expression h can be reached in alternative ways, i.e., it would be equivalent to the classical logical operator "or".

A fact can be considered a particular case of Horn clause when the antecedent does not exist (only consequent exists).

Since in classical logic we define A→B = ¬A∨B and since De Morgan's law ¬(A∧B) = ¬A∨¬B is satisfied, a Horn's clause is

c1, c2, ..., cn → h = ¬ (c1 ∧ ... ∧ cn) ∨ h = ¬c1 ∨ ... ∨ ¬cn ∨ h

A logical expression consisting exclusively of disjunctions is simply called a "clause", where a term and its opposite (or complement) cannot appear, because if they did appear, the clause would be a tautology.

According to classical logic, any logical formula can be expressed in disjunctive normal form (disjunction of conjunctions) or in conjunctive normal form (conjunction of disjunctions). Therefore, a logical formula can be expressed as a conjunction of clauses.

A clause in normal form is a clause in Skolem normal form: existential quantifiers have been made universal by ∃x P(x) = ¬∀x ¬P(x ), where all universal quantifiers appear at the beginning of the expression (prenex form), and where universal quantifiers are eliminated as the variables are considered to be universally quantified.

Inference processes in logic programming are based on classulas and on the "unification" and "resolution" principles of John Alan Robinson [1965].


Unification

Unification is a pattern matching process. Unification attempts to identify expressions by substituting variables (x, y, z) for constants (a, b, c). The unification operator is the substitution operator (=). Two expressions (containing variables) are unified if they have a common expression. Examples:

• f(x, b) = f(a, y) results in x = a and y = b, since the common expression is f(a, b). It is said that f(a, b) is an instance of the two expressions: f(x, b) and f(a, y).
  
  
• f(a, x) and f(x, b ) cannot be unified because x would have to be a and b at the same time.
  
  
• f(a, b) is not an instance of f(x, x) because the two arguments have to be equal.
  
  
• f(x, y) and f(y, z ) can be unified in infinite ways by substituting x, y, z for the same constant, which can be any constant.

It is not necessary to calculate all possible unifiers. It is sufficient to consider the most general unifier, that is, a unifier such that any other unifier can be obtained by instantiating it. In the last example, the most general unifier is x = y = z = a.

The described unification is of first order. Higher order unification is when the variables represent functions.

Robinson introduced unification as a basic operation of his solving principle and developed an algorithm to compute the most general unifier. Robinson's first unification algorithm [1971] was inefficient. Subsequently, more efficient algorithms have been proposed.


Resolution

Resolution is a generalized inference rule that infers a new clause from two clauses containing complementary terms (one is the negation of the other). Formally:

From A∨C and from B∨¬C is inferred A∨B.

The new clause produced (output) is called "resolvent" of the input clauses, in which the complementary terms disappear.

The resolvent rule is a generalization of modus ponens:

From A and from A→B we infer B

Indeed, since A→B is defined as ¬A∨B, applying the resolution rule:

From A and from ¬A∨B we infer B

Examples:

1. From p∨q∨r and from ¬r is inferred p∨q.
2. From p and ¬p we infer □ (the empty clause), which indicates contradiction.

In first-order predicate logic, the resolution rule is:

From P(x) → Q(x) and from P(a) we infer Q(a;)

In clausal form,

From ¬P(x) ∨ Q(x) and from P(a) it is inferred Q(a)

In first-order predicate logic, a unification process is performed. In this case, the unification is x = a. This rule is the one that governs in the syllogism.

Syllogism	Logical Expression	ClauseBB
Everything x that is P, is Q	∀x P (x) → Q(x)	¬P(x) ∨ Q(x)
a es P	P(a)	P(a)
a es Q	Q(a)	Q(a)

The resolution rule also takes this other form:

From P(x) → Q(x) and from Q(x) → R(x) infers P(x) → R(x)

In clausal form,

From ¬P(x) ∨ Q(x) and from ¬Q(x ) ∨ R(x) it is inferred ¬P(x) ∨ R(x)

In this case there is no unification. This rule is the one that governs in the syllogism.

Syllogism	Logical expression	Clause.
Everything x that is P, is Q	∀x P (x) → Q(x)	¬P(x) ∨ Q(x)
All x which is P, is R	∀x Q (x) → R(x)	¬Q(x) ∨ R(x)
All x which is P, is R	∀x P (x) → R(x)	¬P(x) ∨ R(x)

Hiper-resolución

Hyper-resolution is a generalization of resolution in which several resolution steps are combined into one. Basic hyper-resolution consists of splitting the cliques into nuclei and electrons. Nuclei have at least one negative term. Electrons have all positive terms. Hyper-resolution occurs between a nucleus and one or more electrons. There is one electron for each negative term of the nucleus. An electron can be used in more than one intermediate step. Example:

Nucleus: ¬P(x) ∨ ¬Q(x) ∨ R(x)

Electrons: Q(a) ∨ C P(a) ∨ D

Of the nucleus ¬P(x) ∨ ¬Q(x) ∨ R(x) and of the electron Q(a) ∨ C it is inferred ¬P(a) ∨ R(a) ∨ C

From ¬P(a) ∨ R(a) ∨ C and from electron P(a) ∨ D we infer R(a) ∨ C ∨ D

The hyper-resolvable R(a) ∨ C ∨ D can be derived directly (in one step) from the nucleus and the two electrons.

Generalized hyper-resolution consists of considering clauses containing pairs of complementary terms to eliminate them at once. For example:

From A ∨ ¬B ∨ ¬CD ∨ B and E ∨ C it is inferred A ∨ D ∨ E

Resolution by refutation

The resolution rule is also used for the proof of theorems by reductio ad absurdum (resolution by refutation). It is a bottom-up type process (bottom-up):

• If one wants to prove a sentence S, the contrary (¬S) is assumed to be true.
  
  
• The axioms (the Knowledge Base) and the sentence ¬S are converted into clauses.
  
  
• The resolution rule is applied recursively.
  
  
• If at the end an empty clause (□) is reached, which indicates that there is a contradiction, then clause S is a theorem of the original Knowledge Base. If the empty clause is not reached, the clause S is false.

For example, if we have the Knowledge Base

All dogs bark:
∀x (Dog(x) → Bark(x))

Pancho is a dog: Perro(Pancho)

We want to prove S: Some Dog barks: ∃x Barks(x)

1. We convert the Knowledge Base and the ¬S statement into clauses:.
   
   
   Dog(x) → Bark(x) = ¬Dog(x) ∨ Bark(x)
   Dog(Pancho)
   ¬∃x Ladra(x) = ∀x ¬Ladra(x) = ¬Ladra(x).
   
   
2. Applying the resolution to the complementary terms Ladra(x) and ¬Ladra(x), of the first and third clauses, we obtain as resolvent clause ¬Dog(x).
   
   
3. Applying the resolution again to the clauses ¬Perro(x) and Perro(Pancho), we obtain the empty clause (□). Therefore, the clause S is true.

Another example. We have a Knowledge Base formed by the clauses

p ¬q∨¬p∨r q

We want to prove r. We add ¬r as a new clause. Then we have:

From p and ¬q∨¬p∨r we infer ¬q∨r
From ¬q∨r and q we infer r
From r and ¬r we infer □

Therefore, r is true.


The Prolog language

The best known logic programming language is Prolog, which is based on two main concepts:

1. Clausal logic.
   A Prolog program consists of a series of Horn clauses that state the facts and rules of inference. It is the so-called "Knowledge Base".
   
   
2. Automatic inferences.
   It is the control or process associated to how the language obtains the answer to a query related to a Knowledge Base. Inferences are based on the principles of unification and resolution.
   
   Inferences can be of two types: 1) forward chaining (deductive, data-driven); 2) backward chaining (inductive, goal-driven). These inferences are also called top-down and bottom-up, respectively.
   
   Forward inference is the simplest. Backward inference requires a more elaborate process. It consists of stating a goal. Horn's clauses are used to search for the target as a consequent. Once located, the target is replaced by the body of the clause (the antecedent). Each of the conditions of the antecedent are converted into sub-objectives, to which the same mechanism is applied, and so on until all the conditions are met. In the process, all Horn clauses in which the same consequent (objective or subobjective) appears must be considered. The final result is the composition of all the substitutions made.

The limitations of Prolog are:

• Rigid control mechanism.
  In Prolog, limited action can be taken on the control mechanism (to improve efficiency) by means of a so-called "cut operator". In the absence of full control of the process, it is impossible in practice to achieve what is achieved with imperative languages.
  
  
• Horn clauses.
  When talking about logic programming, it is understood that the language relies exclusively on first-order predicate logic. Moreover, in the case of Prolog the restriction is even greater, since it is limited to Horn clauses. It does not support other logics: polyvalent, fuzzy, modal, intuitionistic, etc.
  
  
• Logical relations.
  Prolog is not a "pure" logic programming language, as it includes additional features, such as:
  
  
  • Arithmetic and comparison operators.
    
    
  • An assignment operator (is).
    
    
  • Input/output operations.
    
    
  • The "cut operator", which stops the search for the remaining subgoals of a rule to make the search more efficient or to avoid other unwanted solutions.
    
    
  • Operations to dynamically add or remove rules.
  
  Despite all these "additions", Prolog is far from being a general or universal language.
  
  
• Modifications.
  It allows, in principle, to add knowledge, but not so much to remove it.

Logic Programming with MENTAL
The notation of predicates

In predicate logic, the notation P(x₁, ... , x_n), where P is the predicate and x₁, ... , x_n are the arguments involved in the predicate (n-ary). When n is greater than one, this notation does not clearly reflect the semantic relations of the arguments to the predicate nor the relations of the arguments to each other.

With one argument, there is no problem: Man(Pepe) indicates that Pepe is a man. With two arguments, problems appear: in Father(Pepe, David) it is intuited that it indicates that Pepe is David's father, but the expression does not reflect this. With three arguments, the situation becomes more complicated.

The clearest notation is the one that makes use of MENTAL primitives. Examples:

Pepe/man // Pepe is a man

Father(JosephJohn) = Pepe // Pepe is JosephJohn's father.

Father(Natalia) = Pepe // Pepe is Natalia's father.

Father(Eva) = Pepe // Pepe is Eva's father.

Parent(David) = Pepe // Pepe is David's father.

Pepe's children could be specified in a single expression:

([ (Father([JoséJuan Natalia Eva David]) = Pepe) ])

But the relation "Father" is ascending, which forces to specify in 4 expressions the four children of Pepe or to use the distribution operator. It is simpler to use the descending notation and specify Pepe's children in one expression:

Children(Pepe) = {JoséJuan Natalia Eva David}

This functional type notation has the advantage that it also allows the use of several arguments. For example,

Sons(Pepe Pili) = {JoséJuan Natalia Eva David}

With Pepe/man and Pili/woman.


Knowledge Base

A Knowledge Base consists of:

1. Specific knowledge. In classical terminology, a Factual Basis. It is specified by
   
   ( Facts = ( h1...hn ) )
   
   Being the hi concrete facts.
   
   
2. Generic knowledge. In the classical approach, they are represented by a set of rules:
   
   ( Rules = ( r1...rm ) ) )
   
   Being the ri concrete rules.
   
   The expression of a Horn clause is in MENTAL especially homogeneous:
   
   ⟨ (c1 → c2 → ... → cm) ⟩
   
   In a compact form, it can be expressed as follows: ⟨ →⊣( c1...cm ) ⟩
   
   Specifies that if the conditions c1, ... , c(m−1) are satisfied, then cm is satisfied. This last element we can call the "terminal element" of a Horn clause.
   
   But in MENTAL it is not restricted to Horn clauses nor only to rules. The possible expressions are limited only by primitives.

Knowledge Base Example

1. Specific knowledge (facts).
   
   ( Sons(Pepe Pili) = {JoséJuan Natalia Eva David} )

( Pepe/man Pili/woman )

( JoséJuan/man Natalia/woman Eva/woman David/man )

( Children(Juanjo Natalia) = {Jorge Cristina} )

( Juanjo/man Jorge/man Cristina/woman )
   
   
2. Generic knowledge (rules):
   
   ⟨( (x ∈ Children(y z)) → ((Father(x) = y) (Mother(x) = z))↓ )⟩

⟨( {x y}/Siblings ← ((Father(x) = Father(y) ∧ (Mother(x) = Mother(y)) ∧ x≠y )⟩
   
   Two persons are siblings if they have the same parents or parents (Prog).
   
   ⟨( (Parent(x) = y) → (y/(Prog(x)) )⟩

⟨( (Mother(x) = y) → (y/(Prog(x)) )⟩
   
   The consequents indicate that y is a parent of x. Prog(x) is a qualifier of y.
   
   
3. In addition we can define classes, which are used to perform queries. Examples:
   
   ⟨( (Siblings(x) = Children(Father(x) Mother(x)) ∪' {x} )⟩

⟨( (Prog(x) = {⟨( y ← y/(Prog(x))) )⟩} )⟩

⟨( (Ascendants(x) = {⟨( (y z)↓ ← (x ∈ Offspring(y z)) )⟩} ∪ Ascendants(y) ∪ Ascendants(z) )⟩

⟨( (Descendants(x) = {⟨( y ← ((y ∈ Children(x z) ∨ (y ∈ Sons(z x)) )⟩} ∪ Descendants(y) )⟩

The automatic top-down inference process

The advantage of generic expressions is that, from the initial data (the facts), some results are generated, which feed the generic expressions, which again produce new results, and so on until the results stabilize. This whole process takes place automatically.

1. Rule:
   ⟨( (x ∈ Sons(y z)) → ((Father(x) = y) (Mother(x) = z))↓ )⟩
   
   Results:
   
   Father(JoséJuan) = Pepe) (Mother(JoséJuan) = Pili)
Father(Natalia) = Pepe) (Mother(Natalia) = Pili)
Father(Eva) = Pepe) (Mother(Eva) = Pili)
Father(David) = Pepe) (Mother(David) = Pili)
Father(Jorge) = Juanjo) (Mother(Cristina) = Natalia)
   
   
2. Rule:
   ⟨( {x y}/Siblings ← ((Father(x) = Father(y) ∧ (Mother(x) = Mother(y)) ∧ x≠y )⟩
   
   Results (combinations of siblings taken 2 by 2):
   
   {JoséJuan Natalia}/Siblings
{JoséJuan Eva}/Siblings
{JoséJuan David}/Siblings
{Natalia Eva}/Siblings
{Natalia David}/Siblings
{Eva David}/Siblings
{Jorge Cristina}/Siblings
   
   
3. Rule:
   ⟨( (Parent(x) = y) → (y/(Prog(x)) )⟩
   
   Results:
   
   Pepe/(Prog(JoséJuan))
Pepe/(Prog(Natalia))
Pepe/(Prog(Eva))
Pepe/(Prog(David))
Juanjo/(Prog(Jorge))
Juanjo/(Prog(Cristina))
   
   
4. Rule:
   ⟨( (Mother(x) = y) → (y/(Prog(x)) )⟩
   
   Results:
   
   Pili/(Prog(JoséJuan))
Pili/(Prog(Natalia))
Pili/(Prog(Eva))
Pili/(Prog(David))
Natalia/(Prog(Jorge))
Natalia/(Prog(Cristina))

Knowledge Base Query

Once new results have been generated from the facts and rules, queries can be performed. Queries can be of the selection type or the verification type.

Examples of selection:

1. Who are Pepe's children?
   Sons(Pepe) // ev. {JoséJuan Natalia Eva David}
   
   
2. Who are Pepe's descendants?
   Descendants(Pepe) // ev. {JoséJuan Natalia Eva David Jorge Cristina}
   
   
3. Who are Jorge's ancestors?
   Ascendants(Jorge) // ev. {Pepe Pili Juanjo Natalia}
   
   
4. Who are David's siblings?
   Brothers(David) // ev. {JosephJohn Natalia Eve}
   
   
5. Who are David's parents?
   Prog(David) // ev. {Pepe Pili}
   
   
6. What are the parents with 2 or more children?
   {⟨( (x y)↓ ← (Children(x y))# ≥ 2 )⟩} // ev. {Pepe Pili Juanjo Natalia}

Verification examples:

1. Pepe is male?
   (Pepe/Man)? // ev. α
Pepe/Man is in the Fact Base.
   
   
2. What are Pepe's children?
   Sons(Pepe) // ev. {JoséJuan Natalia Eva David}
Hijos(Pepe) is also in the Fact Base.
   
   
3. Is Pepe the father of David?
   (Father(David) = Pepe)? // ev. α
   
   
4. Are David and Jorge brothers?
   ({David George}/Brothers)? // ev. θ

If clearer answers are desired, we can do:

( (True =: α)(False =: θ) )
(Pepe/man)? // ev. True
(Pepe/woman)? // ev. False


Other attributes

It is also possible to assign other attributes (e.g. numeric) and perform queries, as in Databases. For example, we add the attribute AñoNac (Year of Birth) to Pepe's children in the Fact Base:

( AñoNac(JoséJuan) = 1967 )
( YearNac(Natalia) = 1968 )
( YearNac(Eva) = 1971 )
( YearNac(David) = 1977 )
( YearNac(George) = 1995 )
( YearNac(Cristina) = 1999 )

Who are Pepe's children born in 1970 or later?

{ ⟨( x ← ((Father(x) = Pepe) ∧ (YearNac(x) ≥ 1970) )⟩ } // ev. {Eva David}

Resolution rule

In MENTAL, the resolution rule takes the following form:

⟨( ( ((x ∨ z) (y ∨ ¬z))↓ = (x ∨ y) )⟩

That is, two disjunctive expressions of the abstract spacui containing two opposite terms are replaced by a single one, at all times. The two merging expressions have no relation to each other. They only share the property of belonging to the environment.

This rule is general, valid for all types of expressions x, y, z, whether propositions or predicate logic expressions of any order. It is also a generalized hyper-resolution rule for propositional clausal logic. For example, the clauses

¬P∨¬Q∨R   Q∨C   P∨D

They are solved in two steps:

1. ¬P∨¬Q∨R and Q∨C are transformed into ¬P∨R∨C.
2. ¬P∨R∨C and P∨D become R∨C∨D.

This is another demonstration of the power of generic expressions.


Advantages of MENTAL as a logic programming language

• Language.
  No specialized logic programming language is required.
  
  It provides an integrated, generic and dynamic programming environment in which all the resources available in the language can be used. For example, you can dynamically modify the Knowledge Base, use higher-order rules, combine it with other paradigms, use multi-purpose, modal, fuzzy, intuitionistic logic, etc.
  
  MENTAL is an open language, where the input expressions and those of the program itself have the same semantics and the same syntax.
  
  
• Automatic inferences.
  In MENTAL, generic conditional expressions (parameterized or not), generate inferences automatically from the initial facts.
  
  No inference engine is necessary, as it is provided by the semantics of the language itself through the conditional generic expressions. All inferences are top-down (both specific and generic) and are automatically registered in the environment. The natural inference is the descending one. Unification and resolution mechanisms are not necessary. Everything is simpler and more direct. Unification and resolution mechanisms are useful in automatic theorem proving (when going from general to general), but are not necessary in logic programming (when going from general to particular).
  
  Top-down inference is a very powerful but only a particular case of the immense possibilities of generic expressions.
  
  
• Knowledge Base.
  Knowledge Base queries are conceptually simple and straightforward. They also allow you to define classes, which are really parameterized queries.
  
  Clearly separates specific knowledge from generic knowledge. Traditional notation distinguishes between generic and specific knowledge by the use of variables (x, y, z, ...) or constants (a, b, c, ...). Generic expressions achieve their full meaning by representing generic knowledge. In addition there can be generic expressions of higher order.
  
  It also unifies traditional databases and knowledge bases, in their structural and management aspects.

In conclusion, all the complexity of traditional logic programming lies in:

• The wrong conception of logical implication.
  
  
• The use of quantifiers.
  
  
• The use of bottom-up inference, which is much more complex than top-down inference, which is the natural inference.
  
  
• The use of truth values V and F, instead of existential values.

---

Addenda
On Robinson's principle of resolution

The resolution principle was proposed by Robinson in the 1965 publication "A Machine-Oriented Logic Based on the Resolution Principle" as a foundation for the automatic proof of theorems. Since then, this principle has been applied generally in AI (artificial intelligence).

His method of unification and resolution largely eliminated the combinatorial explosion that occurs in automatic theorem proving, the excessive number of clauses generated, the so-called "Herbrand universes". Actually, the resolution principle rather than "inferring", what it does is to "merge" two clauses into one, with the consequent saving of memory and processing time.

Robinson paved the way for logic programming in general and for the Prolog language in particular.

In Intel, AMD and other microprocessors, an automatic theorem prover (with Robinson's resolution) is used to verify that mathematical operations have been designed correctly.


More information about Prolog

The name "Prolog" comes from "Logic Programming" and was developed in the 1970s by Alain Colmerauer and his team at the University of Marseille, largely inspired by the work on logic programming of Robert Kowalski [1979], who in turn was inspired by Robinson's concepts of unification and resolution by refutation.

The control mechanism uses a backward chaining inference method, since in order to verify a certain initial expression (or objective), the system has to verify whether all the conditions on which it depends (subobjectives) are satisfied, which in turn may or may not depend on other conditions, and so on. What you have in short is a tree in which a depth-first search is performed. The Prolog language has had a great influence on AI. It caused a split between the "Prologists" (the supporters of Prolog) and the "Lispists" (the supporters of Lisp). It is the confrontation between two paradigms: the logical (Prolog) and the functional (Lisp). MENTAL is a language that contemplates, in a simple way, both paradigms and many more. It is a universal paradigm that allows expressing particular paradigms. [see Applications - Artificial Intelligence - MENTAL, an Artificial Intelligence Language].

Prolog has been applied in numerous fields: natural language processing, compiler development, expert systems, pattern search, automatic reasoning, automatic theorem proving, etc.

There are numerous dialects of Prolog, some with particular control mechanisms. The so-called "Edinburgh Prolog" is the "de facto" standardized dialect. There are also "post-Prolog" languages, with more advanced concepts, such as Prolog, which uses an extension of clausal logic and higher-order unification.

Prolog became in the 1980s the official language of the Japanese fifth-generation computer project, based on AI, with parallel processing hardware and Prolog as the logic language for automatic reasoning. The project was cancelled in 1993, after 11 years of development.


Bibliography

• Bramer, Max. Logic Programming with Prolog. Springer, 2013.
  
  
• Bratko, I. Prolog Programming for Artificial Intelligence. Addison-Wesley, 1990.
  
  
• Chang, C.L., Lee, R.C.-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1997.
  
  
• Clocksin, W.P.; Mellish, C.S. Programming in Prolog. Springer-Verlag, 1987.
  
  
• Cuena Bartolomé, José. Lógica Informática. Alianza Editorial, 1985.
  
  
• Hogger, C.J. Introduction to Logic Programming. Academic Press, 1984.
  
  
• Horn, A. On sentences which are true of direct unions of algebras. J. Symblic Logic 16: 14-21, 1951.
  
  
• Kowalski, Robert. Logic for Problem Solving. Elsevier, 1979.
  
  
• Kowalski, Robert. Lógica, Programación e Inteligencia Artificial. Diaz de Santos, 1986.
  
  
• Kowalski, Robert. The case for using equality axioms in automatic demostration. Lecture Notes in Maths, 125: 112-127, 1970.
  
  
• Kowalski, Robert; Frühwirth, Thom. Logic for Problem Solving Revisited. Books on Demand, 2014.
  
  
• Lassez, Jean Louis; Plotkin, Gordon (eds.). Computational Logic. Essays in Honor of Alan Robinson. The MIT Press, 1991.
  
  
• Nadathur, G.; Millar, D. Higher-order Horn clauses. Journal of the ACM, 37 (4): 777-814, 1990.
  
  
• O’Keefe, Richard. The Craft of Prolog (Logic Programming). The MIT Press, 2009.
  
  
• Robinson, John Alan. A machine-oriented logic based on the resolution principle. J. ACM 12 (1): 23-41, 1965.
  
  
• Robinson, John Alan. Automated Deduction with Hyperresolution. International Journal of Com. Mach, 1: 227-234, 1965.
  
  
• Robinson, John Alan; Voronkov, Andrei (eds.). Handbook of Automated Reasoning. The MIT Press, 2001.
  
  
• Robinson, John Alan. Computational Logic: The Unification Computation. Internet, 1971.
  
  
• Sterling, L.S. ; Shapiro, E. The Art of Prolog. MIT Press, 1986.
  
  
• Wang, Hao. Proving Theorems by Pattern Recognition I. Communications of the ACM, 3: 220-234, 1960. Disponible online.