Week S2.5. Recursion and Negation-as-Failure

First-Order definite clause programming

Input: A program $\mathcal{P}$ of FO definite rules, and a conjunctive query:

$$Q=\exists x_1\dots \exists x_m{A}_1\wedge \dots A_n$$

Where $x_1,\dots ,x_m$ are all variables appearing in the FO positive atoms $A_1,\dots ,A_m$.

Output: If $Q$ is a logical consequence of $\mathcal{P}$ then output “Yes” and a substitution of variables in query $Q$, else output “No”.

Resolution

We perform the following algorithm to resolve:

1. Set progress to $\top$.
2. Set current goal to $?A_1,\dots ,A_n$.
3. While the current goal is not empty and progress is $\top$:
   1. Let $\tilde{A}=A_i$ be an atom in the current goal.
   2. If it exists, choose in $P$ a rule $R$ whose head unifies with $\tilde{A}$.
      1. Let '$R=B_1,\dots ,B_m\to H$' be the rule chosen at this step.
      2. If necessary, rename the variables in $R$ to not conflict.
      3. Compute an mgu $S$ for $\tilde{A}$ and the head $H$ of $R$.
      4. In the current goal, replace $\tilde{A}=A_i$ for $B_1,\dots ,B_m$. $?A_1,\dots ,A_{i-1},B_1,\dots ,B_m,A_{i+1},\dots A_n$
      5. Apply $S$ to the current goal.
   3. Set progress to $\perp$.
4. If the current goal is empty and progress is $\top$:
   1. Output “Yes”.
   2. Output the substitution for the variables in the query.
5. Otherwise, output “No”.

Example 1

Consider the following example:

One can travel between any two cities x and y if there is a direct fight from x to y and there is a ticket available to travel from x to y. A ticket between x and y is available if it can be bought online or bought over the phone.

This can be encoded as:

$$\{\begin{array}{l}{D}_f(x,y),T(x,y)\to T_b(x,y)\\ B_o(x,y)\to T(x,y)\\ B_p(x,y)\to T(x,y)\end{array}$$

title: Handling "And" and "Or"
Express $P$ if $A$ and $B$ and $\ldots$ and $Q$:
$$
	A, B, \ldots, Q \rightarrow P
$$
 
Express $P$ if $A$ or $B$ or $\ldots$ or $Q$:
$$
	\begin{aligned}
		A &\rightarrow P \\
		B &\rightarrow P \\
		&\hspace{12px} \vdots \\
		Q &\rightarrow P
	\end{aligned}
$$

Let use consider again the program with extra facts:

$$\{\begin{array}{l}{D}_f(london,paris)\\ D_f(paris,algiers)\\ B_o(london,paris)\\ B_p(paris,algiers)\\ D_f(x,y),T(x,y)\to T_b(x,y)\\ B_o(x,y)\to T(x,y)\\ B_p(x,y)\to T(x,y)\end{array}$$

Thinking about choice points:

Resolution tree

For the given example above, we can produce a resolution tree as such:

Resolution with backtracking

We perform the following algorithm to resolve with backtracking:

1. Set progress to $\top$.
2. Set current goal to $?A_1,\dots ,A_n$.
3. While the current goal is not empty and progress is $\top$:
   1. Let $\tilde{A}=A_i$ be the first atom in the current goal.
   2. If it exists, choose in $P$ the first rule $R$ that has not been chosen yet for the current goal whose head unifies with $\tilde{A}$.
      1. Let '$R=B_1,\dots ,B_m\to H$' be the rule chosen at this step.
      2. If necessary, rename the variables in $R$ to not conflict.
      3. Compute an mgu $S$ for $\tilde{A}$ and the head $H$ of $R$.
      4. In the current goal, replace $\tilde{A}=A_1$ for $B_1,\dots ,B_m$. $?A_1,\dots ,A_{i-1},B_1,\dots ,B_m,A_{i+1},\dots A_n$
      5. Apply $S$ to the current goal.
   3. Else, if there exists a previous goal in the computation history.
      1. Backtrack to the previous goal individuated earlier.
   4. Set progress to $\perp$.
4. If the current goal is empty and progress is $\top$:
   1. Output “Yes”.
   2. Output the substitution for the variables in the query.
5. Otherwise, output “No”.

Example 2

Never-ending resolution

Backtracking does not resolve all the possible issues.

The two programs are logically equivalent, but with the second one the resolution loops and does not give the correct answer; in particular it does not give any answer.

The way in which a program is written matters for the resolution, and this issue cannot be solved; unless we use a completely different algorithm.

Negation as failure

Definite rules do not have negated atoms. To express “someone is innocent if they are not guilty”:

• The following is not a definite rule: $\neg \text{Guilty}(x)\to \text{Innocent}(x)$ and furthermore definite rules cannot have negated atoms as their heads. (no rule can have $\neg \text{Guilty}(x)$ as its head)
• Intuitively, someone is innocent if it is not known that they are guilty.
• So why not say that $\neg \text{Guilty}(x)$ follows from a program if the query "$?\text{Guilty}(x)$" fails?

Closed World Assumption

Closed World Assumption

The closed world assumption is the presumption that what can currently not be shown to be true is false.

This is a different kind of negation for which we use the symbol “not”. Remember that for $\neg A$ to be true, we need to explicitly prove $\neg A$; for this reason '$\neg$' is sometimes called strict negation.

For “not $A$” to be true, we need to show that $A$ is not known to be true; that is to say: every attempt to prove $A$ fails, there is no successful derivation tree for $A$.

Link to original

(Predicate) Logic programming = Definite Clause Programming +

• Control (procedural) features with a selection of leftmost query atom and topmost program rule or fact
• Backtracking to choice points
• Negation as Failure (Closed World Assumption)

A predicate logic programming derivation includes the derivation trees obtained on backtracking in order to prove query and all trees attempting to prove $A$ given a query “not $A$”.

Recursion

Recursion is the process of repeating items in a self-similar way. Recursion in computer science is a method where the solution to a problem depends on the solutions to smaller instances of the same problem.

The smallest instance of the solution to the problem of whether one can travel from $x$ and $y$ is when there is a direct flight from $x$ to $y$:

$$\text{Direct\_flight}(x,y)\to \text{Travel\_from\_to}(x,y)$$

Otherwise, in the general case, the solution to the problem of whether one can travel from $x$ to $y$ depends on a smaller instance of the same problem - whether can one travel from $z$ to $y$ - given that there is a direct flight from $x$ to $z$:

$$\text{Direct\_flight}(x,z),\text{Travel\_from\_to}(z,y)\to \text{Travel\_from\_to}(x,y)$$