Week S2.3. Horn Clauses and Logic Programming

Recap: Using CNF

In this week’s content, need to be familiar with CNF and the rewrite rules.

CNF Rewrite Rules

To obtain CNF, we can perform a series of transformations:

$$\begin{array}{rl}F\to G& \Rightarrow \neg F\vee G\\ F⟺G& \Rightarrow (F\to G)\vee (G\to F)\\ \neg (F\vee G)& \Rightarrow \neg F\wedge \neg G\\ \neg (F\wedge G)& \Rightarrow \neg F\vee \neg G\\ \neg \neg F& \Rightarrow F\\ F\vee (G\wedge H)& \Rightarrow (F\vee G)\wedge (F\vee H)\\ (F\wedge G)\vee H& \Rightarrow (F\vee H)\wedge (G\vee H)\end{array}$$Link to original

For example, transform each formula of ${\Phi }_1$ into CNF:

$${\Phi }_1=\{\begin{array}{llc}1:& P\equiv P& \text{already in CNF}\\ 2:& P\to Q\wedge R\equiv & \text{apply }{R}_1\\ & \neg P\vee (Q\wedge R)\equiv & \text{apply}{R}_2\\ & (\neg P\vee Q)\wedge (\neg P\vee R)& \\ 3:& Q\to S\equiv & \text{apply }{R}_1\\ & \neg Q\vee S& \text{apply }{R}_4\\ 4:& \neg (S\wedge R)\vee T\equiv & \text{apply }{R}_4\\ & (\neg S\vee \neg R)\vee T\equiv & \text{apply associativity of }\vee \\ & \neg S\vee \neg R\vee T& \end{array}$$

We will assign the result for further use to:

$$K{B}_1=\{\begin{array}{ll}1:& P\\ 2:& (\neg P\vee Q)\wedge (\neg P\vee R)\\ 3:& \neg Q\vee S\\ 4:& \neg S\vee \neg R\vee T\end{array}$$

Horn & definite clauses

Horn clause

A Horn clause is a clause in DNF with at most one positive literal. For example, $\neg S\vee \neg R\vee T$ or $\neg Q\vee \neg S$.

Link to original

Definite clause

A definite clause is a clause in DNF with exactly one positive literal and as such is also a Horn clause. For example, $P$ or $P\vee \neg Q$.

Link to original

Definite rules

A definite clause in the form $\neg X_1\vee \dots \vee \neg X_m\vee X$ can be rewritten in the form $\underset{\text{body}}{\underbrace{X_1\wedge \dots \wedge X_m}}\to \underset{\text{head}}{\underbrace{X}}$.

In a program, a rule without a body is also called a fact because it states something that we are sure of.

Link to original

Consider again, $K{B}_1$ from earlier, we can transform the define clauses into definite rules:

$${\mathcal{P}}_1=\{\begin{array}{ll}\to P& \text{(obtained from }P\text{)}\\ P\to Q& \text{(obtained from }(\neg P\vee Q)\text{)}\\ P\to R& \text{(obtained from }(\neg P\vee R)\text{)}\\ Q\to S& \text{(obtained from }\neg Q\vee S\text{)}\\ S,R\to T& \text{(obtained from }\neg S\vee \neg R\vee T\text{)}\end{array}$$

Justification for definite rules (fluff)

We use definite rules as:

• Reasoning over a set $\Phi$ of formulae means being able to decide whether a formula is entailed by the formulas in $\Phi$.
• Reasoning over sets of formula is at the base of many application contexts, from simple automatic reasoning to logical abduction.
• Logical consequence can be defined in terms of models or in terms of natural deduction, which is sound and complete.

It is not always easy to find the right sequence of natural deduction steps, so we can use definite clauses and rules. Given a set $\mathcal{P}$ of definite rules, which is called a program, there is a simple automatic procedure to reason over the rules in $\mathcal{P}$ and decide whether a conjunction of propositional variables is entailed by them.

Definite clauses are important as they can be directly translated into definite rules, hence into a program which we can reason over.

Resolution in propositional definite clause programs

Propositional definite clause program

A propositional definite clause program is a set of definite rules.

Link to original

Conjunctive Query

A (conjunctive) query (CQ) $Q$ is a conjunction of propositions $Q_1\wedge \dots \wedge Q_n$ (also seen as a set $Q_1,\dots ,Q_n$)

Link to original

A CQ $Q$ is a logical consequence or otherwise logically entailed by the program $\mathcal{P}$ denoted $\mathcal{P}\models Q$ if all models of $\mathcal{P}$ are models of $Q$.

To resolve, we use a top-down approach to show logical entailment from a propositional definite clause program by starting from the goal (the proposition(s) of the query) and then we want to decide whether it is / are entailed by the program or not.

Resolution algorithm

Resolution algorithm

Let $\mathcal{P}$ be a definite clause program with rules ${}^{\prime }{B}_1,\dots ,B_m\to H^{\prime }$, where $m\ge 0$, and let ${}^{\prime }?Q_1,...,Q_n^{\prime }$ be a conjunctive query over $\mathcal{P}$.

1. Set progress to $\top$.
2. Set currentGoal to $?Q_1,...,Q_n$.
3. While the currentGoal is not empty and progress is $\top$:
   1. Let $\bar{Q}=Q_i$ be a proposition in the current goal.
   2. If it exists, choose in $\mathcal{P}$ a rule with the head $\bar{Q}$.
      1. Let $B_1,\dots ,B_m\to \bar{Q}$ be a rule in $\mathcal{P}$ with the head $\bar{Q}$.
      2. In the current goal, replace $\bar{Q}=Q_i$ for $B_1,\dots ,B_m$: $?(Q_1,\dots ,Q_{i-1}),(B_1,\dots ,B_m),(Q_{i+1},\dots ,Q_n)$
   3. Else, set progress to $\perp$.
4. If currentGoal is empty and progress is $\top$ then the output is true, otherwise the output is false.

There are two points of non-determinism:

• (3.1) When we choose a proposition in the current goal. The choice here does not matter but we must be consistent, i.e. always leftmost or rightmost.
• (3.2) When we choose a matching rule, this choice does matter. See example 2 for an explanation.

Link to original

Example 1: resolution (step-by-step)

Consider ${\mathcal{P}}_1$ from earlier, is $T$ entailed by ${\mathcal{P}}_1$?

$${\mathcal{P}}_1=\{\begin{array}{ll}\to P& \text{(obtained from }P\text{)}\\ P\to Q& \text{(obtained from }(\neg P\vee Q)\text{)}\\ P\to R& \text{(obtained from }(\neg P\vee R)\text{)}\\ Q\to S& \text{(obtained from }\neg Q\vee S\text{)}\\ S,R\to T& \text{(obtained from }\neg S\vee \neg R\vee T\text{)}\end{array}$$ $$\begin{array}{rl}?& T\\ & \downarrow S,R\to T\\ ?& S,R\\ & \downarrow Q\to S\\ ?& Q,R\\ & \downarrow P\to Q\\ ?& P,R\\ & \downarrow \to P\\ ?& R\\ & \downarrow P\to R\\ ?& P\\ & \downarrow \to P\\ & \top \end{array}$$

Example 2: resolution (step-by-step)

Transform the set $\phi$ of formulas to CNF, then to definite clause program $\mathcal{P}$. Is $S$ entailed by the program?

$$\Phi =\{\begin{array}{l}1:Q\vee P\to S\\ 2:T\wedge G\\ 3:\neg T\vee (G\to P)\end{array}$$

Transformed into CNF:

$$\Phi =\{\begin{array}{ll}1:& Q\vee P\to S\equiv \\ & \neg (Q\vee P)\vee S\equiv \\ & (\neg Q\wedge \neg P)\vee S\equiv \\ & (\neg Q\vee S)\wedge (\neg P\vee S)\\ 2:& T\wedge G\\ 3:& \neg T\vee (G\to P)\equiv \\ & \neg T\vee (\neg G\vee P)\equiv \\ & \neg T\vee \neg G\vee P\end{array}$$

And then into a program:

$$\mathcal{P}=\{\begin{array}{ll}\to T& (\text{from }2)\\ \to G& (\text{from }2)\\ Q\to S& (\text{from }1)\\ P\to S& (\text{from }1)\\ T,G\to P& (\text{from }3)\end{array}$$

Let’s try to evaluate the entailment of $S$ in the previous program via resolution:

$$\begin{array}{rl}?& S\\ & \downarrow Q\to S\\ ?& Q\\ & \downarrow \text{no rule}\\ & \perp \end{array}$$ $$\begin{array}{rl}?& S\\ & \downarrow P\to S\\ ?& P\\ & \downarrow T,G\to P\\ ?& T,G\\ & \downarrow \to T\\ ?& G\\ & \downarrow \to G\\ ?& \top \end{array}$$

Therefore, the choice of the rule at the step where we pick the matching rule influences the evaluation of entailment. We may answer no when the answer is actually true.