Lecture 9. FOL inference

Slides

∀I

Logical methods for AI

Lecture 9

FOL inference

This work is licensed under CC BY 4.0

https://forms.gle/JiXXM9eysAZaJMja9

First Order Inference

Background

Aim: Extend inference methods to FOL
Problem: Undecidability

First Order Natural Deduction

Rules

Two rules per quantifier: $\forall, \exists$

Universal instantiation

Substitution: $A(x)\leadsto A(t)$

If $\forall xA(x)$ is $\forall x\exists y\mathsf{Parent}(x,y)$
... $A(x)$ is $\exists y\mathsf{Parent}(x,y)$
... $A(Ada)$ is $\exists y\mathsf{Parent}(Ada,y)$

Universal instantiation

Only "free":

If $A(x)$ is $\exists y\mathsf{Parent}(x,y)\land \forall x\mathsf{Human}(x)$
... $A(Ada)$ is $\exists y\mathsf{Parent}(Ada,y)\land \forall x\mathsf{Human}(x)$
... not $\exists y\mathsf{Parent}(Ada,y)\land \forall x\mathsf{Human}(Ada)$

Side-condition

No "recapture"

If $A(x)$ is $\exists y \mathsf{Parent}(x,y)$
... we may not infer $\exists y \mathsf{Parent}(y,y)$
... from $\forall x\exists y \mathsf{Parent}(x,y)$

Universal introduction

Side-condition

$\dagger$: $\alpha$ arbitrary

$\alpha$ may not occur in any open assumption for $A(\alpha)$

$$\exists y\mathsf{Friend}(x,y)\nvDash \forall x\exists y\mathsf{Friend}(x,y)$$

Existential introduction

Existential elimination

Side-condition

$\ddagger$: $c$ new
May not occur anywhere in the derivation or KB.
"No assumptions about $c$":

Rules in KBs

$$\forall x\forall n((On(x, n) \land Switch(x, n)) \to Off(x, n + 1))$$ $$\forall x\forall n((Off(x, n) \land Switch(x, n)) \to On(x, n + 1))$$

Inferences

Facts:

$On(L,1)$
$Switch(L,1)$

Generalized MP

Unification

Input: two formulas
Output: substitution that identifies the two.

$$On(L,1)\land Switch(L,1)\text{ and }On(x,y)\land Switch(x,y)$$

$$x\mapsto L, y\mapsto 1$$

Unification

$$\mathsf{YoungerThan}(x,Ada)\qquad \text{ and }\qquad\mathsf{YoungerThan}(Alan,y)$$ $$x\mapsto Alan, y\mapsto Ada$$ $$\leadsto$$ $$\mathsf{YoungerThan}(Alan,Ada)$$

Unification

$$\mathsf{OlderThan}(x,Alan)\qquad\mathsf{OlderThan}(Ada,x)$$ $$x\mapsto Ada, x\mapsto Aland$$ $$\leadsto$$ $$\bot$$

Unification and Generalized MP

First Order Resolution

Resolution rule

$l_{i},k_{j}$ literals:

$$\begin{array}{ccc} l_1\lor l_2\lor \dots\lor p & & \neg p\lor k_1\lor k_2\lor\dots \\ \hline & l_1\lor l_2\lor \dots k_1\lor k_2\lor\dots \end{array}$$ $$\begin{array}{ccc} p & & \neg p \\ \hline & \bot \end{array}$$

$$A\to B\leadsto \neg A\lor B$$ $$\ $$ $$\mathsf{Parent}(\mathsf{FatherOf}(Ada),Ada)\to \mathsf{OlderThan}(\mathsf{FatherOf}(Ada),Ada),$$ $$\mathsf{OlderThan}(\mathsf{FatherOf}(Ada),Ada)\to$$ $$\mathsf{Before}(\mathsf{BirthdayOf}(\mathsf{FatherOf}(Ada)),\mathsf{BirthdayOf}(Ada))\vDash$$ $$\mathsf{Parent}(\mathsf{FatherOf}(Ada),Ada)\to$$ $$\mathsf{Before}(\mathsf{BirthdayOf}(\mathsf{FatherOf}(Ada)),\mathsf{BirthdayOf}(Ada))$$

$$\forall x\forall y(\mathsf{Parent}(x,y)\to \mathsf{OlderThan}(x,y)),$$ $$\forall x\forall y(\mathsf{OlderThan}(x,y)\to \mathsf{Before}(\mathsf{BirthdayOf}(x),\mathsf{BirthdayOf}(y)))\vDash$$ $$\forall x\forall y(\mathsf{Parent}(x,y)\to \mathsf{Before}(\mathsf{BirthdayOf}(x),\mathsf{BirthdayOf}(y)))$$ $$\ $$

Dropped universal quantifiers, renamed variables for uniqueness.
Re-wrote to CNF
Resolution rule with unification: $u\mapsto x$ and $v\mapsto y$.

FOL resolution

$l_{i},k_{j}$ literals:

$$\begin{array}{ccc} l_1\lor l_2\lor \dots\lor m & \neg n\lor k_1\lor k_2\lor\dots \\ \hline & (l_1\lor l_2\lor \dots \lor k_1\lor k_2\lor\dots)[m,\neg n]_U \end{array}$$

FOL CNF

Re-write conditionals: $A\to B\leadsto \neg A\lor B$
De Morgan rules:
- $\neg\neg A\leadsto A$
- $\neg(A\land B)\leadsto \neg A\lor\neg B$
- $\neg(A\lor B)\leadsto \neg A\land\neg B$
Quantifier dualities
- $\neg\forall xA\leadsto \exists x\neg A$
- $\neg\exists xA\leadsto \forall x\neg A$

FOL CNF

Re-name variables: $\forall xA\land \exists xB\leadsto \forall x_1A\land \forall x_2B$.
Apply Skolemization: $$\forall x\exists y(P(x)\to R(x,y))\leadsto\forall x(P(x)\to R(x,f(x)))$$
Drop all the remaining universal quantifiers
Apply the distribution: $$A\lor (B\land C)\leadsto (A\lor B)\land (A\lor C)$$

$$\forall x\forall y(\mathsf{Parent}(x,y)\to \neg \forall z (\mathsf{Parent}(z,y)\to x=z))$$ $$\leadsto$$ $$\forall x\forall y(\neg \mathsf{Parent}(x,y)\lor \neg\forall z(\neg \mathsf{Parent}(z,y)\lor x= z))$$ $$\leadsto$$ $$\forall x\forall y(\neg \mathsf{Parent}(x,y)\lor \exists z\neg (\mathsf{Parent}(z,y)\land x= z))$$ $$\leadsto$$ $$\forall x\forall y(\neg \mathsf{Parent}(x,y)\lor \exists z\neg (\neg\mathsf{Parent}(z,y)\lor x= z))$$

$$\forall x\forall y(\neg \mathsf{Parent}(x,y)\lor \exists z(\neg \neg\mathsf{Parent}(z,y)\land x\neq z))$$ $$\leadsto$$ $$\forall x\forall y(\neg \mathsf{Parent}(x,y)\lor \exists z(\mathsf{Parent}(z,y)\land x\neq z))$$ $$\leadsto$$ $$\forall x\forall y(\neg \mathsf{Parent}(x,y)\lor (\mathsf{Parent}(f(x,y),y)\land x\neq f(x,y)))$$ $$\leadsto$$ $$\neg \mathsf{Parent}(x,y)\lor (\mathsf{Parent}(f(x,y),y)\land x\neq f(x,y))$$ $$\leadsto$$ $$(\neg \mathsf{Parent}(x,y)\lor \mathsf{Parent}(f(x,y),y))\land (\neg \mathsf{Parent}(x,y)\lor x\neq f(x,y)))$$

FOL CNF

The resulting formula is not necessarily equivalent:

$$\nu(\forall x\forall y(\mathsf{Parent}(x,y)\to \neg \forall z (\mathsf{Parent}(z,y)\to x=z)))$$ $$\neq\text{ for some }\mathcal{M}$$ $$\nu((\neg \mathsf{Parent}(x,y)\lor \mathsf{Parent}(f(x,y),y))\land (\neg \mathsf{Parent}(x,y)\lor x\neq f(x,y))))$$

FOL CNF

It is equi-satisfiable:

$$\nu(\forall x\forall y(\mathsf{Parent}(x,y)\to \neg \forall z (\mathsf{Parent}(z,y)\to x=z)))=1$$ $$\text{ for some }\mathcal{M},\alpha$$ $$\Leftrightarrow$$ $$\nu((\neg \mathsf{Parent}(x,y)\lor \mathsf{Parent}(f(x,y),y))\land (\neg \mathsf{Parent}(x,y)\lor x\neq f(x,y))))=1$$ $$\text{ for some }\mathcal{M},\alpha$$