Logic and Logic Programming Definitions

Most of these definitions follow Lloyd [Llo87b].

Unconstrained resolution, while an improvement on its predecessors, is still a massively non-deterministic search through a very large space of possible proofs. Interestingly, there is a class of clauses - the definite clauses - over which a variant of resolution can be made quite efficient.

Assume or give a brief overview of most-general-unifiers. A good overview of resolution theorem proving and its relationship to logic programming is [Rob92].

Atom:

If $p$ is a predicate symbol and $t_i$ are terms, then $p(t_1, ..., t_n)$ is an atom. Note this is at odds with the builtin meta-predicates atom and atomic.

Chronological backtracking:

In Prolog, a failing computation causes a re-examination of the most-recent choice of the clause to execute, in a context where there were several alternatives. The computation proceeds with some other selection.

Clause:

A clause is a logical formula in conjunctive normal form, which has the schema: $p_1 \land ... \land p_m \rightarrow q_1 \lor ... \lor q_n$ or, equivalently, $\lnot p_1 \lor ... \lor \lnot p_n \lor q_1 \lor ... \lor q_n$ where $p_i$ and $q_i$ are atoms.

Clocksin and Mellish [CM81, Appendix B] give a Prolog program to convert arbitrary first-order formulae into clausal form.

Functor:

A function symbol/arity pair. These have the same role as records in other languages (structs in C) which is to aggregate data. These are the data constructors in the context of type systems.

Ground:

A term or atom is ground if it contains no variables.

Horn Clause:

A clause containing at most one positive literal, written (with the commas interpreted as $\land$): $a \leftarrow b_1, ..., b_n$ (a definite clause) or $\leftarrow b_1, ..., b_n$ (a definite goal). Note that introducing negated body goals into the language violates this definition.

Instance of:

One term is an instance of another if it is more instantiated than it, in the sense that it is the result of applying some substitution to the other.

Formally: $\tau$ is an instance of $\rho$ if there exists a substitution $\theta$ such that $\rho\theta = \tau$, written $\tau \preceq \rho$.

Mode:

instantiation states - i.e. whether a variable is bound or free, or in terms of predicates, whether an argument position is an input or an output (or both). Note that the instantiation state of a term can be arbitrarily complex.

Module System:

Some mechanism for dividing a program into separate compilation units, for the purposes of abstraction.

Negation-as-finite-failure:

Prolog uses the closed-world-assumption: if it cannot prove a goal using the clauses in it's database, and the proof attempt fails after a finite number of steps, then the goal is deemed to be false. This rule means that Prolog implements a non-monotonic logic: it is not necessarily the case that adding more clauses to the theory will lead to more things being provable. This is in contrast to classical first-order logic, which is monotonic.

Predicate Symbol:

A predicate symbol is a string/arity pair that names a set of clauses (all of which have the same predicate symbol as heads).

Pure Prolog:

Restriction of the language to Horn clause logic - i.e. no higher-order constructs (call/1, findall/3, ...), meta-predicates (functor/3, arg/3, ...) or built in arithmetic (is/2, ...).

Resolution:

A sound and complete proof technique for first-order clausal logic, invented by Robinson in the early 1960's [Rob92]. Prolog uses a variant of full resolution, where constraints are imposed on clauses and the inputs to the resolution step, called SLD-NF resolution (linear resolution over definite clauses with a selection function, combined with the non-monotonic negation-as-failure rule [Llo87b]).

Substitution:

A substitution is a function that maps a set of variables to a set of terms, and is usually denoted $\theta$. We write $\rho\theta = \tau$ to indicate that the term $\tau$ results when we apply substitution $\theta$ to term $\tau$.

Term:

A term is one of: a variable, a constant symbol (e.g. a numeral), or a compound structure $f(a_1, ..., a_n)$ where $a_i$ are terms. In the latter case, $f$ is called a function symbol, $n$ is the arity of the term, and $f/n$ is the functor.

Type:

A type is a collection of objects deemed to have some common property, such as the set of natural numbers.

Unification:

Unification can be viewed as a generalisation of pattern matching (such as that found in Haskell) in that variables can be bound in both the pattern and the object matched against, rather than just the pattern.

Unification is used in Prolog for assignment, memory allocation, pattern matching, argument binding, etc. As such it can be heavily optimised provided we can discover (essentially) mode information.

More formally, we assume the existence of a sound method of finding the most general unifier (mgu) of two terms, written $\theta = \mbox{unify}(t_1, t_2)$. See [Llo87b] for more details.

Variants:

Two terms are variants if they are identical modulo a variable renaming, which is analogous to $\alpha$-convertibility in the lambda calculus.

If $\tau$ and $\rho$ are variants, we write $\tau \cong \rho$. Obviously $\tau \preceq \rho \land \rho \preceq \tau \Rightarrow \tau \cong \rho$.