Week S2.4. Prenex Normal Form and Unification

Prenex Normal Form

Prenex Normal Form

A formula is in Prenex Normal Form (PNF) if it starts with 0 or more quantifiers followed by a quantifier free formula:

$$Q_1{x}_1\dots Q_n{x}_n\varphi$$

Where $Q_i\in \{\exists ,\forall \}$ and $\varphi$ is quantifier free.

In this case, $Q_1{x}_1\dots Q_n{x}_n$ is the (possibly empty) prefix. And $\varphi$ is the matrix. Any first order formula can be translated into PNF.

Link to original

Examples:

• $\forall x\forall y\neg (P(x)\to Q(y))$
• $\forall x\exists yR(x,y)$
• $R(x,y)$

But not:

• $\forall xP(x)\vee \forall xQ(x)$
• $\neg \forall xR(x,y)$

Algorithm to PNF

Algorithm to Prenex Normal Form

Any first order formula can be converted into Prenex Normal Form by:

1. Eliminate all occurrences of $\to$ and $\leftrightarrow$ from the formula. Use equivalences from propositional logic: $$\begin{array}{rl}\varphi \to \phi & \equiv \neg \varphi \vee \phi \\ \varphi \leftrightarrow \phi & \equiv (\neg \varphi \vee \phi )\wedge (\varphi \vee \neg \phi )\\ \varphi \leftrightarrow \phi & \equiv (\varphi \wedge \phi )\vee (\neg \varphi \wedge \neg \phi )\end{array}$$
2. Move all negations inward, such that negations only appear in front of atoms. Use equivalences: $$\begin{array}{rl}\neg \neg \varphi & \equiv \varphi \\ \neg \exists x\varphi & \equiv \forall x\neg \varphi \\ \neg \forall x\varphi & \equiv \exists x\neg \varphi \end{array}$$
3. Standardise the variables apart where necessary. Renaming variables in a formula such that distinct variables (not in the scope of the same quantifier) have distinct names.
4. The PNF can now be obtained by moving all quantifiers to the front. Use logic equivalences ($x$ not occurring, or already bound, in $\varphi$): $$\begin{array}{rl}\varphi \wedge (\exists x)\phi & \equiv \exists x(\varphi \wedge \phi )\\ \varphi \wedge (\forall x)\phi & \equiv \forall x(\varphi \wedge \phi )\\ \varphi \vee (\exists x)\phi & \equiv \exists x(\varphi \vee \phi )\\ \varphi \vee (\forall x)\phi & \equiv \forall x(\varphi \vee \phi )\end{array}$$ And other equivalences: $$\begin{array}{rl}(Q_{1}x)\varphi \wedge (Q_{2}y)\phi & \equiv (Q_{1}x)(Q_{2}y)(\varphi \wedge \phi )\\ (Q_{1}x)\varphi \vee (Q_{2}y)\phi & \equiv (Q_{1}x)(Q_{2}y)(\varphi \vee \phi )\end{array}$$

Link to original

Example: Transforming to PNF

Transform the formula $\forall x(\exists yR(x,y)\wedge \exists z\neg S(x,z)\to \neg \exists yP(x,y))$. Let’s start by performing steps 1 and 2:

$$\begin{array}{rl}\forall x(\exists yR(x,y)\wedge \exists z\neg S(x,z)& \to \neg \exists yP(x,y))\\ \forall x(\neg (\exists yR(x,y)\wedge \exists z\neg S(x,z))& \vee \neg \exists yP(x,y))\\ \forall x((\neg \exists yR(x,y)\vee \neg \exists z\neg S(x,z))& \vee \neg \exists yP(x,y))\\ \forall x((\forall y\neg R(x,y)\vee \forall z\neg \neg S(x,z))& \vee \forall y\neg P(x,y))\\ \forall x((\forall y\neg R(x,y)\vee \forall zS(x,z))& \vee \forall y\neg P(x,y))\end{array}$$

Then apply step 3:

$$\begin{array}{rl}\forall x((\forall y\neg R(x,y)\vee \forall zS(x,z))& \vee \forall y_1\neg P(x,y_1))\end{array}$$

Finally, apply step 4:

$$\begin{array}{rl}\forall x\forall y\forall z\forall y_1((\neg R(x,y)\vee S(x,z))& \vee \neg P(x,y_1))\end{array}$$

First order Horn clauses

First order Horn clause

A clause in the matrix of a Prenex Normal Form formula is a first order Horn clause if:

• the prefix consists only of universal quantifiers quantifying over all variables in the clause
• the clause consists of a finite disjunction of positive or negative atoms with no more than one positive atom

Link to original

First order definite clause

A first order definite clause is a Horn clause with exactly one positive atom (and 0 or more negative atoms). It is of the form:

$$\forall x_1\dots \forall x_n\neg A_1\vee \dots \neg A_m\vee A$$

Where $m\ge 0$, $A_1,\dots ,A_m,A$ are atoms, and $x_1,\dots ,x_n$ are all the variables appearing in the atoms.

Link to original

First order definite rule

A first order definite clause can be represented as a first order definite rule:

$$\forall x_1\dots \forall x_n\neg A_1\wedge \dots \wedge \neg A_m\to A$$

And we can drop conjunctions for commands:

$$\forall x_1\dots \forall x_n\neg A_1,\dots ,\neg A_m\to A$$Link to original

To PNF to first order definite rules

Given some formula $\varphi$ obtained by transforming to PNF. The matrix of $\varphi$ will be positive or negated atoms joined by the $\vee$ and $\wedge$. In general, one must first transform the matrix of a PNF formula into first order conjunctive normal form in order to identify whether one can then represent it as first order definite rules.

Let $\varphi$ be a PNF formula, If:

1. a clause in the conjunctive normal form of the matrix of $\varphi$ is of the form $\neg A_1\vee \dots \vee \neg A_m\vee A$ ($m\ge 0$)
2. the prefix of $\varphi$ contains universal quantifiers that quantify over every variable in $\neg A_1\vee \dots \vee \neg A_m\vee A$

Then the clause is a definite clause and can be represented as a definite rule.

First order (predicate) definite clause programming

First order definite clause program

A first order definite clause program is a set of first order definite clauses, these can be represented as their equivalent definite rules.

Link to original

First order conjunctive query

Let $\mathcal{P}$ be a program of first order definite rules. A conjunctive query $Q$ to $\mathcal{P}$ is a prenex normal form formula:

$$Q=\exists x_1\dots \exists x_n{A}_1,\dots ,A_m$$

Where $A_1,\dots ,A_m$ is a conjunction of positive atoms. Where $x_1,\dots ,x_n$ are the variables in $A_1,\dots ,A_m$.

Link to original

Example: Resolution over first order definite rules

For example, given we have:

$$\mathcal{P}=\{\begin{array}{ll}1:& \to \text{Loves}(john,mary)\\ 2:& \to \text{Engaged}(john,mary)\\ 3:& \forall x\forall y\text{Loves}(x,y),\text{Engaged}(x,y)\to \text{Marries}(x,y)\end{array}$$

We can have a first order conjunctive query:

$$?\exists z\exists w\text{Marries}(z,w)$$

Just as with propositional logic, we expand selected query atoms by choosing a rule with a matching head. Then replace the atom in the query with the body of the rule.

$$\begin{array}{lc}\text{?}& \exists x\exists w\text{Marries}(z,w)\\ & \downarrow \begin{array}{l}\forall x\forall y\text{Loves}(x,y),\text{Engaged}(x,y)\to \text{Marries}(x,y)\\ [x/z,y/w]\end{array}\\ \text{?}& \exists x\exists w\text{Loves}(z,w),\text{Engaged}(z,w)\\ & \downarrow \begin{array}{l}\to \text{Loves}(john,mary)\\ [z/john,w/mary]\end{array}\\ \text{?}& \text{Engaged}(john,mary)\\ & \downarrow \begin{array}{l}\to \text{Engaged}(john,mary)\\ []\end{array}\\ & \top \end{array}$$

Referring to the unification we learn about below:

• $\{(x/z),(y/w)\}$ is an mgu of $\text{Marries}(z,w)$ and $\text{Marries}(x,y)$.
• $\{(z/john),(w/mary)\}$ is an mgu of $\text{Loves}(z,w)$ and $\text{Loves}(john,mary)$.

Substitutions & Unification

Substitution

A substitution $S$ is a finite set $\{(x_1/t_1),\dots ,(x_n/t_n)\}$ where:

• $x_1,\dots ,x_n$ are distinct variables (only variables can be substituted)
• $t_1,\dots ,t_n$ are terms (variables, constants, or functional terms)

If we let $S$ be a substitution and $\varphi$ a first order formula, then $S(\varphi )$ is the result of applying the substitution $S$ to $\varphi$.

Link to original

Unifier

If we let $S$ be a substitution and $\varphi$ and $\phi$ be two first order formulas: Then $S$ unifies, or is a unifier for, $\varphi$ and $\phi$ if $S(\varphi )=S(\phi )$.

Link to original

Example: From Slides

{
	"url":"[10b_unification.pdf](https://git.is.horse/insert/university/obsidian-notes/-/raw/9d95afcbbdb7a4c77ca9f62b32e35c6f31e269e7/University/Year%201/Semester%201%20%26%202/4CCS1ELA%20Elementary%20Logic%20with%20Applications/Slides/10b_unification.pdf)",
	"page":[6,7,8,9],
	"scale":1.7
}

Most general unifiers

Two formulas that unify might have different unifying substitutions:

1. $m(x,y)$ and $m(a,z)$ are unified by $S=\{(x/a),(y/z)\}$, so we have that: $S(m(x,y))=m(a,z)=s(m(a,z))$
2. $m(x,y)$ and $m(a,z)$ are unified by $T=\{(x/a),(y/b),(z/b)\}$, so we have that: $S(m(x,y))=m(a,b)=s(m(a,z))$ Here, $T$ makes unnecessary substitutions.

Most general unifier

$S$ is the most general unifier of $F_1$ and $F_2$ if and only if, for all other unifiers $T$, there is some substitution $S^{\prime }$ such that $T(\{F_1,F_2\})=S^{\prime }(S(\{F_1,F_2\}))$.

Link to original