FOL Inference

Logical methods for AI

FOL Inference

Lecture 9

What you’ll be able to do

FOL inference

True in every model of the premises?
How can a computer establish this?

FOL consequence

Formula SQL

Each query starts from the displayed model. Powered by sql.js

Enable JavaScript to use the model canvas. The definitions and worked examples remain available.

Countermodels

A countermodel (glossary, opens in a new tab) makes the premises true and the conclusion false: $\forallx (Human(x) \to Mortal(x)), Mortal(Socrates) ⊭ Human(Socrates)$

Formula SQL

Each query starts from the displayed model. Powered by sql.js

Enable JavaScript to use the model canvas. The definitions and worked examples remain available.

Deciding consequence

The halting problem (glossary, opens in a new tab) can be encoded in FOL inference.

Unifiers

Examples:

$A = Human(x)$ and $B = Human(Socrates)$ . Unifier: $[x/Socrates]$
$A = R(x, y)$ and $B = R(z, z)$ . Unifier $[x/a, y/a, z/a]$ , but MGU = $[x/z, y/z]$
$A = Human(a)$ , $B = Mortal(a)$ . No unifier!

Robinson’s algorithm

Clause form

Examples:

$\forallx (Human(x) \to Mortal(x))$ : the clause $(\negHuman(x) \lor Mortal(x))$
$\existsx Human(x)$ : replacing it by $Human(a)$ claims more.

Equisatisfiability

$\existsx Human(x)$ and $Human(sk₁)$ , for a fresh $sk₁$ :

A human exists: interpret $sk₁$ as one.
$Human(sk₁)$ is true: a human exists.

Not equivalent: with a human in $D$ and $⟦sk₁⟧$ the mouse, $\existsx Human(x)$ is true and $Human(sk₁)$ false.

Skolemization

Rewriting:

$\forallx\existsy R(x,y) ⟹ \forallx R(x,sk₁(x))$
$\existsy\forallx R(x,y) ⟹ \forallx R(x,sk₁)$

Skolemization, step by step

FOL resolution

Refutations

Refutation completeness

Standardizing apart: $\negP(f(x))$ , renamed $\negP(f(y))$ , resolves with $P(x)$ by $[x/f(y)]$ .
Factoring: $(P(x) \lor P(y))$ becomes $P(y)$ by $[x/y]$ .
Fair search (glossary, opens in a new tab) finds a refutation if there is one, and may run forever on $P(a)$ , $P(f(a))$ , …

Quantifier rules

Side conditions

Blocked by a side condition

$\forall Intro$

$x$ must not be free in an open assumption.

$\forall Elim$

The term must be free for $x$ : here $\existsy$ captures $y$ . $\exists Intro$ has the same condition.

$\exists Elim$

The witness $z$ must be fresh: not free in the conclusion, in the existential premise, or in an open assumption.

Two quantifiers

Quantifiers in Lean

A Boolean law in Lean

leanexample : ∀ x : Bool, (!!x) = x := by
  intro x
  have step_1 : (!!x) = (!!x) := by
    rfl
  have step_2 : (!!x) = ((!!x) && true) := by
    exact Eq.subst (Eq.symm (Bool.and_true (!!x))) step_1
  -- steps 3 to 12: distributivity, complementation, identity, commutativity
  have step_13 : (!!x) = x := by
    exact Eq.subst (Eq.symm step_12) step_6
  exact step_13

Each have states and proves one step of the derivation of $NOT NOT X = X$ .
by simp finds a proof; Lean’s kernel checks it.

Open the full proof in L∃∀N (opens in a new tab)