Lecture 8

FOL

Johannes Korbmacher Lecture slides

Logical methods for AI

FOL

Lecture 8

What you’ll be able to do

fol_ai_talking_folΡδx|x - c | < δ|f(x) - f(c)| < ΡxyF(x,y) = -F(y,x)

All humans are mortal

  • Propositional logic: HUMAN₁ β†’ MORTAL₁, HUMANβ‚‚ β†’ MORTALβ‚‚, …
  • First-order logic: βˆ€x (Human(x) β†’ Mortal(x))

Alphabet

Terms

The interactive tree is loading. The explanation in the chapter can also be followed without it.

Enable JavaScript to step through the tree. The grammar and worked example remain available in the chapter.

Formulas

  • Atomic: Human(Socrates), motherOf(x) = y
  • Quantified: βˆ€x (Human(x) β†’ Mortal(x))
  • A term, not a formula: fatherOf(Socrates)

Scope and binding

Enable JavaScript to explore variable binding.

Models

Reasoning scenario
sun SUN ↦ 1rain RAIN ↦ 1
Basic facts
⟦Human⟧
Objects and relations

First-order models

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

Domain and interpretation

fol_domain_big1ΰ² _ΰ² Soda23

Classical FOL assumes nonempty domains, a referent for every name, total functions and a truth-value for every atom: idealizations.

Denotation

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

Assignments and denotation

Model checking

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

Satisfaction

Quantifiers

  • βˆƒx: one witness is enough.
  • βˆ€x: one counterexample refutes it.
gimmick_mouse

Extensions

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

Models as databases

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

1
2
3
4
5
6
7
8
9

CREATE TABLE BiggerThan (
  bigger TEXT NOT NULL,
  smaller TEXT NOT NULL,
  PRIMARY KEY (bigger, smaller)
);
INSERT INTO BiggerThan VALUES
  ('sir', 'jimmy'),
  ('jimmy', 'box'),
  ('sir', 'box');

An extension becomes a table; a tuple, a row.

Queries as open formulas

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

Formulas to SQL

Each free variable ranges over Domain; query(A) is the condition for A.

FOLSQL condition
LocatedIn(x, Europe)EXISTS (SELECT 1 FROM LocatedIn AS r WHERE r.country = d.value AND r.continent = 'Europe')
Β¬ANOT (query(A))
A ∧ B(query(A)) AND (query(B))
A ∨ B(query(A)) OR (query(B))
βˆƒy AEXISTS (SELECT 1 FROM Domain AS e WHERE query(A))
βˆ€y ANOT EXISTS (SELECT 1 FROM Domain AS e WHERE NOT (query(A)))

Queries and Codd’s theorem

gimmick_database