This chapter merges two decks: M8 — Logic & Computation, the theory lecture, and C3 — Prolog: Fast Track, the lab case study. They are the two halves of one arc: M8 builds computational logic up to SLD resolution and stops at the door of a language; C3 walks through that door and writes programs. Sections 1 to 9 are M8, sections 10 to 12 are C3, and the section on the parent/grandparent example belongs to both, since both decks use it.
Logic is the study of correct reasoning, especially as it involves the drawing of inferences. It studies the way we draw conclusions and express ourselves, and deals with how to formalise that [Metakides and Nerode, 1996]. It dates back to Aristotle, for whom logic is the instrument for human knowledge [De Rijk, 2002].
Computational logic (CL) is logic in computer science [Lloyd, 1990]. The deck’s formulation of its scope is worth memorising because it is a three-part list, not a slogan: it concerns all uses of logic in computer science — to compute, to represent computation, and to reason about computation. It is rooted in logic, applied mathematics, artificial intelligence and computer science.
After a long lack of interest, at the end of the seventeenth century Gottfried Leibniz observed — quite in isolation — that if ideas are concepts like numbers, they should be representable and manipulable in the same way as numbers, clearly bridging logic and mathematics for the first time [Levesque, 2012], crediting Ramon Llull’s Ars Generalis (1308) as an inspiration.
A formalism for mathematics is typically credited to George Boole, from the middle of the nineteenth century [Boole, 2009]: along with Augustus De Morgan, they started extending logic to become a tool for the study of the foundations of mathematics. Logic finally regained centrality in Western thought with Gottlob Frege, who introduced the first formal language for logic and mathematics, to ground mathematical reasoning on a sound basis [Frege, 1971].
Then the crisis. Starting from a paradox in Cantor’s theory of numbers, Russell’s paradox — the set of all sets that do not belong to themselves — exposed the logical inconsistencies at the foundations of mathematics. This made clear that only a rigorous formalisation could lead to well-founded mathematical reasoning and theories. Around 1920 Hilbert’s programme aimed at addressing the issue, and the acme of those efforts was the Principia Mathematica [Whitehead and Russell, 1927], a complete logic formalisation of all mathematics treated as a whole axiomatic system — soon to be undermined by Gödel’s incompleteness theorems [Gödel, 1931].
The deck introduces the central distinction with two examples that are worth keeping side by side.
So there are two ways to set the truth of a sentence: by considering it as a sequence of symbols and manipulating them independently of their meaning; or by interpreting the symbols and considering the truth of the meaning of the sentence.
Alfred Tarski [Tarski and Tarski, 1994] formalised the notion of logical interpretation as the relation between the symbols (syntax) and the elements of the domain of discourse (semantics). And he defined logical entailment, or logical consequence, precisely: when a conclusion is true in every interpretation making all premises true, then the premises logically entail the conclusion.
From which the deck draws a chain of consequences that motivates everything after it. If a conclusion is true for any interpretation, it is true independently of the interpretation, hence independently of the semantics of symbols; and if it is true independently of the semantics of symbols, it would likely depend on symbols only; therefore the syntactic notion of truth is in principle connected with logic entailment.
If p and q hold, does r hold too? Interpret p as “all men are mortal”, q as “Socrates is a man”, r as “Socrates is mortal”, and we know it does. Interpret p as “Charles drives a beautiful and fast red car”, q as “Max drives an unreliable blue car”, r as “Kimi drives a horrible and slow silver car”, and we do not know. Since there is at least one interpretation by which r is not true given p and q, r is possibly true, yet is not a logical consequence of p and q.
If p and p → q hold, does q hold too? Whichever our interpretation of p and q, q is always true given p and p → q. Since its truth value does not depend on the interpretation of symbols, q is a logical consequence of p and p → q.
After Tarski’s work, logic is typically discussed as a two-sided story [Levesque, 2012]: a syntactic side involving axioms and rules of inference — sometimes called a proof theory; and a semantic side involving interpretations and truth — sometimes called a model theory; with soundness and completeness theorems relating the two sides.
Pfenning’s formulation, quoted by the deck, is the pivot of the whole module:
To compute we start from a given expression and, according to a fixed set of rules (the program), generate a result. For example, 15 + 26 → (1+2+1)1 → (3+1)1 → 41.
To deduce we start from a conjecture and, according to a fixed set of rules (the axioms and inference rules), try to construct a proof of the conjecture. For example, we conjecture that an + bn ≠ cn for n > 2.
→ So computation is mechanical and requires no ingenuity, while deduction is a creative process. For example, proving that an + bn ≠ cn for n > 2 basically took 357 years of hard creative work.
Roughly, then: computation can be thought of as an automatic process and delegated to a machine, while deduction requires some form of intelligence. In restricted areas the two can be unified [Pfenning, 2007] — Boolean algebras, for instance. More generally, even if we follow a well-defined set of formal rules, we know that not everything we can reason about is mechanically computable, given the fundamental undecidability results.
Yet the two do meet, in both directions. Computation can be seen as a limited form of deduction, since it establishes theorems: 15 + 26 = 41 is both the result of a computation and a theorem of arithmetic. And deduction can be considered a form of computation if we fix a strategy for proof search, removing the guesswork — and the possibility of employing ingenuity — from the deductive process. That is, if we automate deduction. As Pfenning puts it, this latter idea is the foundation of logic programming: logic program computation proceeds by proof search according to a fixed strategy; by knowing what this strategy is, we can implement particular algorithms in logic, and execute the algorithms by proof search.
Now the move that makes this a chapter of this course rather than a logic lecture. The possibility of choice, of deliberation, is a key issue in the relationship between computation and deduction. “Removing the guesswork” from the deductive process, fixing a strategy for proof search, means there is no longer space for choice. So autonomous choice and rational deliberation are required whenever deduction is required and computation cannot be implemented as an automatic technique. In the deck’s own words: whenever computation and deduction do not exactly match, there lies the space for autonomy.
And then the deck immediately objects to itself, which is why the passage is worth reading twice. Wait: autonomous computation is still computation; in principle, it cannot be used to bridge the gap between deduction and computation. True. The resolution: the relationship between deduction and computation is stated independently of the domain of discourse, hence independently of specific knowledge about the domain — which is precisely what mathematicians use when they try to prove theorems. So in order to instrument and exploit autonomous choice in the space between deduction and computation in non-trivial domains, knowledge about the specific domain is required, leaning onto the semantic side, and can be used to drive the choices whenever an automatic strategy does not exist — for instance, to determine which path to follow in the proof tree.
This is the same discovery Chapter 6 recorded historically, arriving here by a formal route. There, the way out of the AI winter was that humans use extensive domain knowledge to cut down the search space. Here, domain knowledge is what an autonomous agent needs in order to choose in the gap between what is mechanically computable and what must be deduced. Two vocabularies, one insight: knowledge is what makes choice tractable.
A judgement is an object of knowledge — knowing a judgement comes from the evidence we have for it [Martin-Löf, 1996]. The most common judgement is A true: given a proposition A, A is true. Most of logic programming deals with the truth of propositions. Other judgements exist: A false, for true negation; A true at t, the subject of temporal logic; K knows A, the subject of epistemic logic.
The most interesting evidence is a proof. Let J, J1, ..., Jn be judgements and R an inference rule: a deduction is a proof that can be read equivalently as “if J1 and ... and Jn, then we can conclude J by virtue of rule R”, or “given J1 ... Jn, we can prove J by rule R”, or “J can be deduced or inferred from J1 ... Jn by means of rule R”. J1 ... Jn are the premises and J is the conclusion, written as a fraction with the premises above the line, the conclusion below, and R labelling the line.
If we know J1 ... Jn and the rule concluding J from them, we can infer J. How do we know, say, J1? We may know J1,1 ... J1,n and a rule R1 concluding J1 from them. Thus we may build an inference chain to prove J — if possible.
Given the structure of a deduction, the data structure covering all possible inference chains for a judgement J is a proof tree: whose root is the conclusion J; whose edges are deductions labelled by an inference rule; and where premises are child nodes and conclusions are parent nodes.
What are the leaves? Where do we start with our deductions? Is there any judgement that can be said to be true without proof? This is the role of axioms: an axiom is, in logic, an indemonstrable first principle, rule or maxim that has found general acceptance or is thought worthy of common acceptance, whether by virtue of a claim to intrinsic merit or on the basis of an appeal to self-evidence. Axioms can be used as premises in a proof tree with no need of proof.
How do we explore the proof tree? Should we start from what we know and try to prove our conjecture, deduction after deduction? Or start from the conjecture, find the deductions that prove it, and try to prove the premises, recursively? Or build the tree in some other way and explore it with some other strategy?
| Strategy | How it goes | Direction in the tree |
|---|---|---|
| Forward chaining forward-reasoning search | We start from what we know (initially, the axioms); we exploit inference rules to deduce new judgements (theorems); we add new evidence to the old one; recursively; until we obtain our conjecture | From the leaves down to the root |
| Backward chaining goal-directed search | We start from what we need to prove (initially, the conjecture); we exploit inference rules to find the judgements it depends upon; we find new judgements to prove; recursively; until we end up depending only on the axioms | From the root up to the leaves |
Both strategies seem to fit computation, but the deck raises four questions — would this be a deterministic computation? would it converge? would it actually terminate? could it be a parallel, concurrent or distributed computation? — and answers them preliminarily:
Start from what you know — initially the axioms — exploit inference rules to deduce new judgements, add the new evidence to the old, recursively, until the conjecture is obtained. It traverses the proof tree from the leaves down to the root. It is data-driven: you find out what follows from what you have.
Start from what you need to prove — initially the conjecture — use inference rules to find the judgements it depends upon, and recursively prove those, until you depend only on axioms. It traverses the tree from the root up to the leaves. It is goal-directed, and it is what SLD resolution does: resolution leads to backward chaining, from goal back to axioms.
A definite clause A ← B1, ..., Bm read declaratively says: A is true if B1, ..., Bm are true. This is a statement about the world, with no notion of execution in it. Aristotle’s sense of declarative is a sentence that can be said either true or false, so declarative programming means programming through true sentences declaring what to compute — the meaning.
The same clause read procedurally says: to prove A, prove B1, ..., Bm. Now it is a procedure declaration, and calling it means proving its subgoals. Procedural programming is programming through operational statements determining how to compute — the method. And the point of the whole chapter: for logic programs the two interpretations coincide [Kowalski, 1974], which is a property logic programming languages such as Prolog are the only ones to hold [Metakides and Nerode, 1996].
The early history [Apt, 2005]: automatic deduction of theorems; first-order logic by Frege, Peano and Russell; computation as deduction by Gödel and Herbrand; and the resolution principle by Robinson [1965], along with unification.
Resolution allowed the proof of first-order theorems and made it possible to compute with logic — but not yet to see logic as a full computational framework. Something was still missing between computable logic and logic as a programming language.
What was missing was the procedural interpretation of Horn clauses. By defining logic programs as collections of Horn clauses, and by restricting Robinson’s principle accordingly, Kowalski showed how a logical implication could be amenable to both a declarative and a procedural interpretation [Kowalski, 1974], thus providing the foundations for a logic programming language. Prolog, by Colmerauer in Marseille, came along in 1973. As Colmerauer and Roussel later put it: there is no question that Prolog is essentially a theorem prover à la Robinson; our contribution was to transform that theorem prover into a programming language.
| Feature | Content |
|---|---|
| terms | Computing takes place over the domain of all terms defined over a “universal” alphabet |
| mgu | Values are assigned to variables by means of automatically-generated substitutions, called most general unifiers. These values may contain variables, called logical variables |
| backtracking | The control is provided by a single mechanism: automatic backtracking |
Two further properties are worth recording. Logic programs can be seen as executable specifications: the logic programmer is concerned with what to compute, while how to compute — the control — is delegated to the underlying logic programming machinery. Sometimes this could lead to inefficiency. And logic programming languages can be seen as formalisms for either executable code or knowledge representation, which makes them languages for artificial intelligence.
Finally, interactive programming: the model behind computation-as-deduction natively supports writing a logic program and then interacting with the logic machinery by means of multiple queries, or by asking for multiple solutions. Logic languages intrinsically support the interactive style of programming and computing — a feature useful in distributed systems too, supporting notions such as LPaaS, Logic Programming as a Service [Calegari et al., 2018].
Logic programming is ruled by different principles from other programming paradigms: atomic actions are equations between terms, executed by means of the unification process trying to solve them; unification assigns values to variables; and values can be arbitrary terms — in fact there is just one sort of variable, ranging over the set of all terms.
The definition is recursive:
Let X, Y be variables, a, b constants, f and g functors of arity 3 and 2. Then a, b, X, Y are proper terms; f(a,b,a) and g(X,Y) are proper terms; f(a, X, g(Y,b)) is a proper term. Variables and constants are atomic terms; terms built out of proper functors are structured terms. In f(a, X, g(Y,b)), f is the functor symbol of arity 3, and a, X, g(Y,b) are the three subterms.
Remarks that matter: the definition is recursive, leading to a recursive data structure — a tree. Terms are fundamental in mathematical logic and essential in computer science: they capture both arithmetic expressions and strings. No specific alphabet is assumed — a universal alphabet for all terms. And no meaning is a priori attached to symbols, in particular to functors: + is just a functor, not associated a priori with the plus sign of arithmetic. Hence: no types.
Logic programs compute over the truth values of sentences, so how do we write sentences? We know how to denote the elements of the domain of discourse, not yet how to talk about them. Sentences in logic are typically called propositions.
Predicates do the job. If p is a predicate symbol of arity n and t1, ..., tn are terms, then p(t1, ..., tn) is an atom. Atoms represent elementary propositions in logic programming; if A is an atom, then A is a logic formula stating that A is true.
Negation makes it possible to deal with false propositions: if A is an atom, ¬A is a logic formula stating that A is false, and A, ¬A are literals. Literals can be combined through logical connectives: conjunction A ∧ B, disjunction A ∨ B, implication A → B, equivalence A ↔ B.
A logic clause is a finite disjunction of literals [Console et al., 1997]. If A1, ..., An, B1, ..., Bm are atoms containing variables X1, ..., Xk, then
∀X1...Xk (A1 ∨ ... ∨ An ∨ ¬B1 ∨ ... ∨ ¬Bm)is a logic clause, logically equivalent to
∀X1...Xk ((A1 ∨ ... ∨ An) ← (B1 ∧ ... ∧ Bm))usually written simply as A1, ..., An ← B1, ..., Bm. A clausal normal form (CNF) is a conjunction of clauses.
Now the restriction that makes logic programming possible:
| Kind | Shape | Condition | In a logic program |
|---|---|---|---|
| definite clause | A ← B1, ..., Bm | exactly one positive literal (n = 1) | a rule |
| unitary clause | A ← | one positive, no negative literal (n = 1, m = 0) | a fact |
| definite goal | ← B1, ..., Bm | no positive literal (n = 0) | a goal |
| Horn clause | — | either a definite clause or a definite goal (n = 1 or n = 0) | — |
Hence: a logic program is a CNF of Horn clauses, that is, a conjunction of rules and facts (and goals).
Two things from this section are asked constantly. First, what makes a clause a Horn clause: at most one positive literal — one for definite clauses, none for goals. Second, why the restriction matters: Robinson’s resolution principle works for general clauses and shows that it is possible to compute by contradiction whether a CNF entails a formula, but it does not provide a proof strategy for a full-fledged programming language; restricting to Horn clauses and recasting the principle accordingly gives SLD resolution, and with it the procedural interpretation that coincides with the declarative one.
Robinson’s resolution principle works for general clauses: given a CNF H and a formula F, it shows that it is possible to compute (by contradiction) whether H logically entails F — however, it does not provide a proof strategy for a full-fledged logic programming language. Kowalski showed this could be obtained by restricting logic programs to CNFs of Horn clauses and recasting Robinson’s principle accordingly: the so-called SLD-resolution principle [Nilsson and Maluszynski, 1995].
Proving proceeds by contradiction. Robinson’s principle tries to prove a formula F false against a CNF H, succeeding if this fails — technically, proving that H ∪ ¬F is not satisfiable. Proving an atom G in logic programming amounts to proving ¬G against logic program P, that is, proving goal ← G on P. Computation in logic programming proceeds by proving goals, and resolution leads to backward chaining, from goal back to axioms.
To prove a goal G with respect to program P, the resolution principle proceeds according to the procedural interpretation. First we look for one clause A ← B1, ..., Bn in P whose head A unifies with G. If the most general unifier of G and A is θ, then the proof of G succeeds if we can further prove B1θ, ..., Bnθ — where Biθ represents the application of the mgu to Bi. The application of θ to the clause specialises it to the specific atom we need to prove, and resolution proceeds recursively with the proof of the subgoals. In general, the computational state of SLD resolution includes a (possibly empty) conjunction of atoms to be proven — the current goal.
How it ends, if it does:
The inference rule itself, in the deck’s notation:
← A1, ..., Ai-1, Ai, Ai+1, ..., Am B0 ← B1, ..., Bn
------------------------------------------------------------------
← (A1, ..., Ai-1, B1, ..., Bn, Ai+1, ..., Am)θwhere A1...Am are atomic formulas and ← A1, ..., Am is the conjunction of subgoals to prove; B0 ← B1, ..., Bn is a definite clause in program P (n ≥ 0), suitably renamed with new and unique variable names to avoid name clashes; and there is an Ai unifying with B0 such that mgu(Ai, B0) = θ.
SLD resolution is non-deterministic in two independent ways:
The choice does not affect correctness of the resolution, so we could choose non-deterministically. But how to exploit either or-non-determinism or and-non-determinism, or both, determines how the automatic resolution process explores the proof tree. And different computational models — sequential, parallel, concurrent — could be exploited: more clauses with a unifying head could be used for goal proof at the same time, either in parallel or concurrently.
Both decks use the same program, so it is the natural place to see everything at once:
parent(joey, luca).
parent(joey, simone).
parent(lino, joey).
parent(mirella, joey).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).Declaratively: four facts expressed by predicate parent/2 — four propositions considered true with no need of proof, our axioms; a possible interpretation is that joey is a parent of luca, just one of the many, even though the most intuitive for English speakers. One rule expressed by grandparent/2, short for ∀X,Y,Z: grandparent(X,Z) ← parent(X,Y), parent(Y,Z), meaning that the formula grandparent(X,Z) holds if both parent(X,Y) and parent(Y,Z) are true, whatever the values of X, Y, Z.
Procedurally: two procedures are defined, parent/2 and grandparent/2, and two kinds of call can be executed. To compute parent/2 we use the four facts, non-deterministically. To compute grandparent/2 we use the rule, first matching the rule head, then proceeding by calling the two subprocedures via the two subgoals of the form parent/2.
And the possible goals, with their answers:
| Goal | Outcome |
|---|---|
grandparent(lino, luca) | succeeds — one refutation, no computed substitution |
grandparent(lino, joey) | fails — no refutations |
grandparent(lino, X) | succeeds twice — X/luca, X/simone |
grandparent(X, simone) | succeeds twice — X/lino, X/mirella |
grandparent(X, Y) | succeeds four times — X/lino Y/luca; X/lino Y/simone; X/mirella Y/luca; X/mirella Y/simone |
?- grandparent(lino, X), ending in the empty goal. The dashed arrow is the choicepoint Prolog remembers: automatic backtracking is the single control mechanism of the language, and it is what turns one refutation into two answers.Everything above was about logic programming in general. Prolog is a particular language, with particular lexical conventions and one particular search strategy.
| Category | Convention |
|---|---|
| Variables | Alphanumeric strings starting with an uppercase letter or an underscore. The underscore alone is the anonymous variable, a sort of don’t-care variable; an underscore followed by a string is a normal variable during resolution, but does not need to be exposed in the computed substitution |
| Functors | Alphanumeric strings starting with a lowercase letter — this holds for both proper functors and constants |
| Terms | Built recursively out of functors and variables, as in logic programming: term, Var, f(X), p(Y,f(a)) are Prolog terms; term, var, f(a), p(x,y) are ground terms |
| Predicates | Alphanumeric strings starting with a lowercase letter — the same as functors |
| Atoms | Built by applying predicates to terms: predicate, f(X), p(Y,f(a)) are Prolog atoms |
And a remark that opens a door: out of context, parent(lino,joey) could represent either a ground atom or a ground term. Is this an issue or a feature? It paves the way towards meta-programming.
Clauses follow the shape of Horn clauses, with Prolog punctuation:
| Clause | Form | Condition |
|---|---|---|
| clause | A :- B1, ..., Bn. | A is the head, B1...Bn the body, :- denotes logic implication, . is the terminator |
| fact | A. | a clause with no body (n = 0) |
| rule | A :- B1, ..., Bn. | at least one atom in the body (n > 0) |
| goal | :- B1, ..., Bn. often written ?- B1, ..., Bn. | no head, at least one atom in the body |
A Prolog program is a sequence of Prolog clauses, interpreted as a conjunction of clauses, constituting a logic theory made of Horn clauses written according to Prolog syntax.
The aim of a Prolog computation: given a program P and the goal ?- p(t1,...,tm) — also called a query — if X1...Xn are the variables in the terms, the meaning of the goal is to query P and find whether there are values for those variables that make the query true. The aim is thus to find a substitution σ = X1/s1, ..., Xn/sn such that P ⊨ p(t1, ..., tm)σ.
As a logic programming language, Prolog adopts SLD resolution. As a search strategy, it applies resolution in a strictly linear fashion: goals are replaced left to right, sequentially; clauses are considered in top-to-bottom order; subgoals are considered immediately once set up. The result is a depth-first search strategy. And in order to achieve completeness, Prolog saves choicepoints for any possible alternative still to be explored, going back to the nearest available choicepoint in case of failure — exploiting automatic backtracking.
The framework used in the lab is SWI-Prolog, available at its home site, on GitHub, and online as SWISH, where you write the program on the left, the goal on the bottom right, and press CTRL-ENTER.
The deck lists seven things to observe while interacting with these programs, and they are a good checklist for anyone new to the paradigm: success; failure; computed substitution; unification; backtracking; clause order; and no input/output parameters — no direction is required for arguments, in principle, thanks to unification.
The last item is the one that most surprises programmers coming from other paradigms, and it is the practical face of the declarative/procedural coincidence. sum(X, Y, Z) is not a function from two inputs to one output: it is a relation, and any subset of its arguments may be bound. That is why ?- sum(X, s(s(z)), s(s(s(s(s(s(z))))))) is a legitimate question, and why the same predicate both checks and computes and generates.
In pure logic programming — and in pure Prolog — 3 and + are just symbols with no specific meaning attached. So how do we deal with natural numbers? Giuseppe Peano shows us the way.
The five Peano axioms, introduced in 1889, were meant to provide a rigorous foundation for the natural numbers, and in particular they enable an infinite set to be generated by a finite set of symbols and rules: (1) zero is a natural number; (2) every natural number has a successor in the natural numbers; (3) zero is not the successor of any natural number; (4) if the successor of two natural numbers is the same, then the two original numbers are the same; (5) if a set contains zero and the successor of every number in the set, then the set contains the natural numbers.
To represent them in logic programming we use constants and functors for the numbers, and predicates for relations such as n ∈ ℕ. From the axioms: zero is essential, so we use the constant z; and the notion of successor is essential, so we use the functor s/1. If N is a natural number then s(N) is another natural number — a recursive data structure, where the successor of s(N) is s(s(N)). In our pre-interpretation, z is zero, s(z) is one, s(s(z)) is two. And the predicate nat/1 represents the relation: nat(s(s(z))) means that two is a natural number, according to our current interpretation.
Three remarks close the section, and the first is the one students get wrong: z is zero, 0 is not zero. Recursive data structures are powerful and expressive, yet unreadable for humans and generally impractical — which is why Prolog is actually impure logic programming, offering things like ?- X is 1 + 3. Logic programming allows for the generation of data, for instance the set of natural numbers. There is an unlimited number of SLD refutations here: an infinite branch of the proof tree. And the order of clauses matters in Prolog — what if we exchanged the fact with the rule?
Both remarks are traps with the same root: Prolog is a strategy layered on top of a logic. Logically, the order of clauses is irrelevant — a program is a conjunction, and conjunction is commutative. Operationally, Prolog considers clauses top to bottom and depth first, so putting the recursive rule before the base fact turns a terminating program into a non-terminating one without changing its meaning. Likewise 0 is not zero because nothing in the logic attaches arithmetic to symbols: meaning comes from the program, not from the glyph.
Lists are defined via two constructors: nil, the empty list containing no elements; and cons, taking an element H and a list T and generating the list cons(H, T). So cons(a, cons(b, cons(c, nil))) would represent the list a, b, c. They are typical recursive data structures, used to represent sequences of any sort.
In Prolog the two analogous constructors are [] for the empty list — a constant — and . for cons, a functor of arity 2, so that cons(H,T) is .(H,T). Prolog sequence notation simplifies writing lists: .(H,T) can be written [H|T]; .(H,.(H2,T2)) can be written [H,H2|T2]; and there the empty list can be omitted. So [a,b,c] represents the list a, b, c, where a is the head, [b,c] is the tail, and:
mgu([a, b, c], [H|T]) = {H/a, T/[b, c]}Being recursive data structures, lists are typically handled by recursive rules — which is incidentally also the only way to handle repeated operations over sequences in Prolog, where there is nothing like a cycle programming construct. The recursion scheme follows from the search strategy: since Prolog is depth-first, with clauses used orderly top-down, termination is handled with a fact, typically coming before the recursive rule — exactly as in nat/1 and sum/3.
Checking whether the first argument is a term that is a member of the list in the second argument:
member(X, [X|_]).
member(X, [_|T]) :- member(X, T).Goals to try, and to discuss:
?- member(b, [a,b,c]).
?- member(b, [a,b,b]).
?- member(X, [a,b,c]).
?- member(blue(X), [red(a), blue(b), red(c), blue(d)]).
?- member(z, X).The remarks the deck attaches: the search strategy goes left to right through the list; the program devises out all the members of the list; it supports conditional membership, given a certain computed substitution — which is what the blue(X) goal exercises; and it supports the generation of lists, which is what the last goal does, since member(z, X) with X unbound asks for lists containing z rather than testing a given one.
Two clauses, five completely different behaviours — test, count, enumerate, pattern-match, generate — and not one line of control flow anywhere. That is what “the logic programmer is concerned with what to compute, while how to compute is delegated to the machinery” means in practice, and it is also why Chapter 7 could describe a BDI intention as a stack of plans handled “similarly to how a Prolog interpreter handles clauses”.
Logic in computer science: it concerns all uses of logic in computer science — to compute, to represent computation, and to reason about computation. It is rooted in logic, applied mathematics, artificial intelligence and computer science.
Semantic: “the sum of numbers two and one is three” is true in any formalisation of arithmetic, whatever symbols we use — truth through interpretation. Syntactic: if “the Snark was a Boojum” then “something is a Boojum” is true whatever the meaning of the sentence — truth through symbol manipulation alone.
Tarski: when a conclusion is true in every interpretation making all premises true, the premises logically entail the conclusion. If a conclusion is true for any interpretation it is true independently of the interpretation, hence independently of the semantics of the symbols; and if so, it likely depends on the symbols only — therefore the syntactic notion of truth is in principle connected with logical entailment. Example: p and p → q entail q, whatever p and q mean.
To compute we start from a given expression and, according to a fixed set of rules (the program), generate a result — 15 + 26 → 41. To deduce we start from a conjecture and, according to a fixed set of rules (axioms and inference rules), try to construct a proof — for instance that a^n + b^n ≠ c^n for n > 2, which took 357 years of hard creative work. Computation is mechanical and requires no ingenuity; deduction is a creative process.
(1) Computation can be seen as a limited form of deduction, since it establishes theorems: 15 + 26 = 41 is both a computation result and a theorem of arithmetic. (2) Deduction can be considered a form of computation if we fix a strategy for proof search, removing the guesswork and the possibility of ingenuity — that is, if we automate deduction. The latter is the foundation of logic programming: computation proceeds by proof search according to a fixed strategy.
Fixing a strategy for proof search removes the space for choice, so autonomous choice and rational deliberation are required whenever deduction is needed and computation cannot be implemented as an automatic technique: whenever computation and deduction do not exactly match, there lies the space for autonomy. The self-objection: autonomous computation is still computation, so in principle it cannot bridge the gap. The resolution: the relation between the two is stated independently of the domain of discourse, so exploiting autonomous choice in non-trivial domains requires domain knowledge, leaning onto the semantic side, which can drive the choices — for instance which path to follow in the proof tree.
The data structure covering all possible inference chains for a judgement J: its root is the conclusion J, its edges are deductions labelled by inference rules, and premises are child nodes while conclusions are parent nodes. Its leaves are axioms — indemonstrable first principles that can be used as premises with no need of proof.
Forward (forward-reasoning search): start from what we know, initially the axioms; use inference rules to deduce new judgements; add new evidence to old, recursively, until the conjecture is obtained — traversing the tree from the leaves down to the root. Backward (goal-directed search): start from what must be proven, initially the conjecture; use rules to find the judgements it depends on; recursively prove those until only axioms remain — traversing from the root up to the leaves. Resolution leads to backward chaining.
Robinson’s resolution principle [1965], with unification, allowed proof of first-order theorems and made it possible to compute with logic, but did not provide a proof strategy for a full-fledged language. Kowalski [1974] supplied the procedural interpretation of Horn clauses: by defining logic programs as collections of Horn clauses and restricting Robinson’s principle accordingly, a logical implication became amenable to both a declarative and a procedural interpretation. Prolog followed, by Colmerauer in Marseille, in 1973.
A term is: a variable; or a functor of arity 0, that is a constant; or f(t1,...,tn) where f is a functor of arity n and the ti are terms. Variables and constants are atomic terms, the rest are structured terms, and the recursive definition makes a term a tree. An atom is p(t1,...,tn) where p is a predicate symbol of arity n; atoms represent elementary propositions. A literal is an atom A or its negation ¬A.
A logic clause is a finite disjunction of literals. A definite clause has exactly one positive literal, A ← B1,...,Bm; a unitary clause is a definite clause with no negative literals, A ←; a definite goal has no positive literal, ← B1,...,Bm. A Horn clause is either a definite clause or a definite goal. A logic program is a CNF of Horn clauses — a conjunction of rules (definite clauses), facts (unitary clauses) and goals.
To prove goal G against program P, look for a clause A ← B1,...,Bn whose head A unifies with G; if mgu(G,A) = θ, the proof of G succeeds if we can further prove B1θ,...,Bnθ, the mgu specialising the clause to the goal at hand; and resolution proceeds recursively. Endings: the current goal becomes empty, giving a successful derivation, an SLD refutation; a selection rule picks the next subgoal when it is not empty; the selected goal matches no clause head, so the proof fails; or the goal never empties while heads keep matching, so the derivation does not terminate.
Or-non-determinism: more than one clause could unify through its head with the current goal, and either could be chosen for the resolution step. And-non-determinism: more than one goal could be subject to proof at the same time, and either could be chosen, through a selection rule. Neither choice affects correctness, but how they are exploited determines how the proof tree is explored — and both admit parallel, concurrent or distributed exploitation.
SLD resolution applied in a strictly linear fashion: goals replaced left to right, sequentially; clauses considered top to bottom; subgoals considered immediately once set up — hence a depth-first search. To achieve completeness Prolog saves choicepoints for every alternative still to be explored, returning to the nearest one on failure through automatic backtracking, which is the single control mechanism of the language.
Following Peano: the constant z for zero and the functor s/1 for successor, so that s(z) is one and s(s(z)) is two, with the predicate nat/1 for the relation of being a natural number. The base fact nat(z). plus the recursive rule nat(s(N)) :- nat(N). give a finite representation of infinitely many propositions. The trap: z is zero, 0 is not zero — no meaning is attached a priori to symbols. A second trap: clause order matters operationally, so putting the recursive rule before the base fact breaks termination without changing the logical meaning.
member(X,[X|_]). and member(X,[_|T]) :- member(X,T). The goals demonstrate a search strategy going left to right through the list; the devising of all members of a list; conditional membership given a computed substitution, as in member(blue(X), [red(a), blue(b), red(c), blue(d)]); and the generation of lists, as in member(z, X) with X unbound.