2. Clauses and Substitutions

Clauses, facts, rules and goals

A Horn clause is a disjunction of literals of which at most one may be positive. A Horn clause with one positive literal is called a Definite clause.

Special definite clauses:

• Fact

  A definite clause comprising a single positive literal $A$ is called a fact. These are unconditional statements about the world. They can be used in the base case of recursive definitions and in Prolog must appear before rules, for example:

  factorial(0,1).
  factorial(X,N) :- X>0, X1 is X-1, factorial(X1,N1), N is X*N1.

  Link to original

• Rule

  A definite clause with some negative literals is called a rule.

  Link to original

Programs are sets of definite clauses, so they are composed of facts and rules. A Horn clause that only contains negative literals is called a goal, it can be thought of as a query to the program.

The implication $(B_1,B_2,\dots ,B_n)\to A$ is read: ”$A$, if $B_1$ and $B_2$ and $\dots$ and $B_n$”, and hence “if” is represented by the symbol :-, and the conjunction by a comma ,, giving:

A :- B1, B2, ..., Bn

Role of variables in clauses and programs

Used in a program, all clauses are individually universally quantified on all variables. For example, the clauses:

$$\begin{array}{r}\text{likes}(X,P)\vee \neg \text{based}(P,Y)\vee \neg \text{likes}(X,Y)\\ \text{attends}(X,Y)\vee \neg \text{registered}(X,Y)\vee \neg \text{likes}(X,Y)\end{array}$$

Actually represent the universally quantified formulas:

$$\begin{array}{r}\forall X\forall P\forall Y((\text{based}(P,Y)\wedge \text{likes}(X,Y))\to \text{likes}(X,P))\\ \forall X\forall Y((\text{registered}(X,Y)\wedge \text{likes}(X,Y))\to \text{attends}(X,Y))\end{array}$$

Writing Horn clauses using Prolog syntax

• Horn clause with one positive literal and no negative literals is a Prolog fact:

  rainy(tuesday).
  temperature(tuesday, celsius(0)).

• Horn clause with one positive literals and some negative literals is a Prolog rule:

  snowy(x) :- rainy(x), temperature(X, celsius(Y)), Y =< 0.

• Horn clause with only negative literals is a Prolog goal or query:

  :- snowy(X).

Consider the definitions above, the informal procedural mechanism works as such:

• We try to solve the goal :- snowy(X) by looking for clauses with the predicate in the head
• If a match is found, we replace snowy(X) by the body of the matching clause, replacing variables are required for the matching
• New goal is :- rainy(X), temperature(X, celsius(Y)), Y =< 0.
• We continue by replacing X by tuesday: :- temperature(tuesday, celsius(Y)), Y =< 0
• The next literal can be solved by replacing Y with 0, yielding goal 0 =< 0 which also succeeds. Hence the original goal succeeds.

Example rewrites of each well-formed rule, fact or goal, using Prolog syntax.

Rule, fact or goal	Prolog
$p(g(Y),a)$	p(g(Y), a).
$\neg p(X,a)\vee \neg q(Y)$	:- p(X,a), q(Y)
$q(f(Y,a))\vee \neg q(X)\vee \neg p(Y,g(a))$	g(f(Y,a)) :- g(X), p(Y, g(a))
$\neg q(f(a,g(Y)))$	:- q(f(a, g(Y))).
$q(a)\vee p(b,g(X))$	Not a Horn clause.

Variable Substitutions

A substitution is a partial mapping from variables to terms, with a finite domain.

• A substitution $\sigma$ is written as a mapping $\{X_1\mapsto t_1,\dots ,X_n\mapsto t_n\}$.
• $\text{dom}(\sigma )$ denotes the domain of the substitution $\{X_1,\dots ,X_n\}$.

We replace variables with terms as only variables can be replaced and not all terms are variables.

A substitution $\sigma$ is applied to a term $t$ or literal $L$ by simultaneously replacing in $t$ or $L$ each variable occurring in $\text{dom}(\sigma )$ by terms associated to the variable in $\sigma$. The result is denoted $t_{\sigma }$ (term) or $L_{\sigma }$ (literal).

Replacements for a given set must be simultaneous, e.g. $\sigma =\{X\mapsto Y,Y\mapsto a\}$.

If we were to apply this left-to-right, we would replace $X$ by $a$ in $t$. We actually want to replace both $X$ and $Y$ at the same time.

Substitutions represent variable bindings and are used in the instantiation of universally quantified variables.

Consider the following program $P$ and a goal :- r(a).

p(a).
p(b).
q(a).
 
% bind X to any arbitrary, but same, variable in p and q
r(X) :- p(X), q(X).
 
% we can now query
r(a)