First Order Predicate Calculus
If your thesis is utterly vacuous
Use first-order predicate calculus.
With sufficient formality
The sheerest banality
Will be hailed by the critics: "Miraculous!"
-- Henry Kautz
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
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
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,
"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
Person(Mary), Loves(Romeo, Juliet), Hates(father(Romeo),father(Juliet))
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
Symbols are just that, arbitrary names whose semantics is determined
by the interpretation: Hates(father(Romeo),father(Juliet))
could be expressing that √ (36) > √(100),
evaluating to FALSE.
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.
2 * 7 = 14. Person(Mary), Hates(FatherOf(Juliet), Romeo).
Degree of abstraction can vary depending on the ambitions of the
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
relations. It leads to the Frame Problem: we also have to
keep track of everything that does NOT change (!!) when some action is
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
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).
(Dog(x)) -- here x is a free
∃ x (Dog(x)) -- here x is a bound
- 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
∀ x . Dog(x) ⇒ Animal(x) .
∀ 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)
∃ 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
"Everyone loves somebody":
∀ x. ∃ y. Loves(x,y)
Everyone, say x, loves at least one other person y, but who y is
depends on who x is.
∃ y. ∀ x. Loves(x,y)
There exists a single person y who is loved universally by all other
Typical and fine English sentence:
"People only vote against issues they hate". (Really? that's ALL
Models for FOL
Problem: combinatorics. E.g. just with
p k-ary predicates and n constants, there are
p nk 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
- 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
integers or people we can use our intuitions to guide proofs.)
- "Chess is the crucible for Artificial Intelligence" (Donald
Really? Do we need grandmaster knowledge, deep strategies? With
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).
Next Big Topic
Inference with Resolution.