173 Lectures

Why FOPC (FOL)?

PC is weak: can't express "All classes are boring", "Some people like some cats", "If anyone moves, you all die."

FOL is not all-powerful by any means:

no concept of time
hard to do arithmetic
can't do beliefs --"If he believes this then surely he must believe that" is often wrong in everyday life; also surprising mathematical results.
Can't have variables with set values: "All functions are boring" turns out to be a 2nd-order, not 1st-order statement.

FOPC (FOL) Facts

FOL has variables, universal and existential quantification (infinite AND and OR), predicates that assert properties of things, and functions that map between things.

FOL has practical advantages, especially for automation. At least one sound and complete rule of inference (resolution), a semi-decidable inference procedure.

FOL can be written in non-clausal or clausal syntax. The former is more "human-friendly", with (more or less) intuitive operators. Latter is better for computers; harder for humans to see semantics of a sentence (recall a clause is just a disjunction of literals):
A imples B, A → B vs. ( ∼ A ∨ B)

Thus non-clausal proof techniques (with several inference rules), clausal-techniques (one rule, calls for putting sentences into CNF).

"Theorem proving" can be used, as in prolog, for question-answering, but also for planning (generating a sequence of actions for a robot, say).

"Close" to being powerful enough for actual practical use, has been extended as we've seen with times, quantities, math, modal operators...

Individuals, Terms, Predicates, Functions

In a domain including people with some named individuals we might have FOL:
Person(Mary), Loves(Romeo, Juliet), Hates(father(Romeo),father(Juliet))
Where
the term Mary is a named domain element
the predicate Person is unary
the predicate Loves is binary
the function father is unary, evaluates to a person's father.

The symbols used (Juliet, father) need to be given an interpretation (what's a function, a predicate, etc.), and individuals must be mapped onto domain elements before truth value can be assigned to a sentence.

Symbols are just that, arbitrary names whose semantics is determined only by the interpretation: Hates(father(Romeo),father(Juliet)) could be expressing that √ (36) > √(100), thus evaluating to FALSE.

FOL Formulae

Complex expressions are formed using the connectives ∧ , ∨, ⇒, ⇔ as in propositional logic, along with quantifiers ∃, ∀ . Term: a constant or variable (coming up!), or function applied to an appropriate number of terms.

Ground Term: a term with no variables.
E.g. Plus(2,3), MotherOf(FatherOf(Fred)).

Atomic formula (atom, atomic well-formed-formula (WFF)) : A predicate applied to an appropriate number of terms.
E.g. 2 * 7 = 14. Person(Mary), Hates(FatherOf(Juliet), Romeo).

Degree of abstraction can vary depending on the ambitions of the formulator! E.g...

Eat(Joe, Cookie) , (past, present, future..?)
Eat (Joe, Cookie1> , Eat-event3) ∧ Cookie(Cookie1) ⇒
Inside(Cookie1, Joe, Result-state(Eat-event3))

This last is like the Situational Calculus, a way of keeping track of time and causation by identifying events and formalizing their relations. It leads to the Frame Problem: we also have to keep track of everything that does NOT change (!!) when some action is taken.

FOL Semantics

Goal: determine if a formula is TRUE or FALSE. For this, need an interpretation to specify:

Domain of individuals
One domain element for each constant symbol
Functions: N individuals → 1 individual, for each function symbol.
E.g. Son(Mary, Bill) ⇒ Tom.
Relations over domain (set of ordered k-tuples of individuals) for each predicate symbol.
E.g. Older(Tom, Ted) ⇒ FALSE
Assign truth values (TRUE or FALSE) to atoms from domain.
Assign truth values to WFFs (e.g. by using truth tables).

Quantification and Variables

Express properties of entire collections of individuals without referencing each by name. We use a variable to stand for all the individuals.

The variable is bound by the quantifier. This introduces the familiar idea of scoping in a logic context, usually disambiguated by parentheses ().

Quantifiers may be iterated and nested.

Usually variables are late letters (...,x,y,z).

Existential Quantification: An OR (∨) over the relevant individuals. Read as "There Exists or There Is (at least one)". E.g.
∃ x (Dog(x)) -- here Dog() is a predicate, x is the variable. Meaning: "There is a dog" (but we don't know which one).
Binding:
(Dog(x)) -- here x is a free (unbound) variable.
∃ x (Dog(x)) -- here x is a bound variable.
Universal Quantification: An AND (∧) over the relevant individuals. Read as, and meaning, "For All". E.g.
∀ x (Dog(x) ⇒ Animal(x)) -- Every dog is an animal. Or, with . meaning "scope extends to end of sentence, ∀ x . Dog(x) ⇒ Animal(x) .

Examples

∀ x(Dog(x)) ⇒ ∃ y[Person(y) ∧ Owns(y,x)]
-- Every dog is owned by someone.
∃ x ∃ y ∃ e. Eat(x,y,e) ∧ Dog(x) ∧ Cookie(y) ∧ Eat-event(e)
-- A dog eats (ate, will eat) a cookie.
∃ x. Dog(x) ∧ Owns (John, x) -- John has a dog.

∀, ∃ related: No whale is a fish.
∀ x. Whale(x) ⇒ ∼ Fish(x)
∀ x. Fish(x) ⇒ ∼ Whale(x)
∀ x. ∼ (Whale(x) ∧ Fish(x))
∀ x. ∼ Whale(x) ∨ ∼ Fish(x)
∼ ∃ x. Whale(x) ∧ Fish(x)

∀ , ∃, More Examples

Ambiguity in English

Totally pervasive!

"Everyone loves somebody":

Either
∀ x. ∃ y. Loves(x,y)
Everyone, say x, loves at least one other person y, but who y is depends on who x is.
or
∃ y. ∀ x. Loves(x,y)
There exists a single person y who is loved universally by all other people x.

Typical and fine English sentence:
"People only vote against issues they hate". (Really? that's ALL people do?).

Models for FOL

Problem: combinatorics. E.g. just with p k-ary predicates and n constants, there are p n^k instantiations.

Inference in First-Order Logic

Simple Modus Ponens, Universal Instantiation

Universal Instantiation brings in idea ofthe substitution of an individual for a variable. Along with two-way matching (unification), basic to automated proof. We'll be back to this!

Soon we'll see Existential Instantiation: if we know
∃ x. P(x), for example, we know there is at least one individual A such that P(A). If we know who it is, well enough, but even if not we are entitled to imagine the individual and call him anything we want, like Fred, P, Skolem-constant, whatever. We simply invent a name for the individual for later use. We'll use this rule of inference, Skolemization later, also in the context of automated proofs.

Generalized Modus Ponens, Forward Chaining

Generalized Modus Ponens, Backward Chaining

Non-clausal FOL Inference

We've only seen examples using non-clausal syntax and (generalized) Modus Ponens, but there are LOTS of valid inference rules! Contrapositive, for instance, exchanging ∀ , ∃, ∼ .... etc! So if we want to automate:

What syntax? Non-clausal? OR is there better idea?
What inference rule to use at any given time? Strategy? Semantics?
What arguments to supply to predicates and functions for a proof? If we see A-Predicate(x,y) ⇒ z , what should we substitute for the variables from our on-going proof to use that fact?
Non-clausal proofs bring in judgement, semantics (if the proof is about integers or people we can use our intuitions to guide proofs.)
"Chess is the crucible for Artificial Intelligence" (Donald Michie). Really? Do we need grandmaster knowledge, deep strategies? With enough computer power, maybe we can just search (a la Deep Blue).
Hence is born automatic theorem proving with one representation (clauses from CNF), one inference rule (resolution), and the technical necessity of unification (binding variables).

First Order Predicate Calculus

Good Advice