First-Order Logic Fundamentals
undefined
First-order Logic
Some slides are borrowed from Chelsea Finn & Nima Anari
Limitations of propositional logic
Propositional logic is rather limited in its expressive power.
E.g., “For every x, x > 0” is true if x is a positive integer.
We cannot say it in propositional logic.
Nor can we show the following logical equivalences:
"Not all birds fly" is equivalent to "Some birds don't fly".
"Not all integers are even" is equivalent to "Some integers are not even".
"Not all cars are expensive" is equivalent to "Some cars are not expensive“.
We need first-order logic.
CS411: Artificial Intelligence I, Bing Liu
2
Outline
Syntax
Semantics
Inference based on modus ponens
Inference based on classic reasoning
Summary
3
CS411: Artificial Intelligence I, Bing Liu
Syntax of first-order logic
Terms
(refer to objects):
Constant symbol (e.g., Arithmetic) – starts with a capital letter
Variable (e.g., x)
Function of terms (e.g., Sum(3, x))
Formulas
:
Atomic formulas (atoms):
predicate
applied to terms (e.g.,
Knows(x, Arithmetic))
Connectives applied to formulas (e.g., Student(x) → Knows(x, Arithmetic))
Quantifiers applied to formulas (e.g.,
∀
x Student(x) → Knows(x, Arithmetic))
CS411: Artificial Intelligence I, Bing Liu
4
Predicate
P
r
e
d
i
c
a
t
e
:
A
p
r
e
d
i
c
a
t
e
i
s
a
p
r
o
p
e
r
t
y
a
b
o
u
t
o
f
s
o
m
e
o
b
j
e
c
t
s
o
r
a
r
e
l
a
t
i
o
n
s
h
i
p
a
m
o
n
g
o
b
j
e
c
t
s
r
e
p
r
e
s
e
n
t
e
d
b
y
t
h
e
v
a
r
i
a
b
l
e
s
.
Example
"The sky is blue”
"The cover of this book is blue"
For the above two sentences, we can use
is_Blue
as the
predicate. We can also simply use
B
.
B(x), where x is variable representing an arbitrary object.
B(x) reads as "x is blue".
CS411: Artificial Intelligence I, Bing Liu
5
Another predicate example
"John gives the book to Mary",
"Jim gives a loaf of bread to Tom", and
"Jane give a lecture to Mary"
All can be expressed using this predicate:
Give(x, y, z)
which reads, x gives y to z.
E.g., Give(John, Book, Mary), Give(Jane, Lecture, Mary)
CS411: Artificial Intelligence I, Bing Liu
6
Quantification
A predicate with variables is not a
proposition
(with truth value of
T or F).
E.g., the statement
x >
1 with variable
x
over the universe of real numbers
is neither true nor false since we don't know what
x
is.
It can be true or false depending on the value of
x
.
For
x >
1 to be a proposition either
we substitute a specific number for
x,
or
change it to something like "There is a number
x
for which
x >
1 holds", or
"For every number
x
,
x >
1 holds".
We are using
quantifiers.
CS411: Artificial Intelligence I, Bing Liu
7
From predicate to propositions
A
predicate
with variables (called an
atomic formula
) can be made
a
proposition
by applying one of the following two operations to
each of its variables:
assign a value to the variable
quantify the variable using a
quantifier
Let us use predicate
GreatThan(x, 1)
to represent x >1.
u
n
i
v
e
r
s
a
l
q
u
a
n
t
i
f
i
e
r
:
“
f
o
r
e
v
e
r
y
o
b
j
e
c
t
x
i
n
t
h
e
u
n
i
v
e
r
s
e
,
x
>
1
”
w
r
i
t
t
e
n
a
s
:
x
G
r
e
a
t
T
h
a
n
(
x
,
1
)
e
x
i
s
t
e
n
t
i
a
l
q
u
a
n
t
i
f
i
e
r
:
"
f
o
r
s
o
m
e
o
b
j
e
c
t
x
i
n
t
h
e
u
n
i
v
e
r
s
e
,
x
>
1
“
w
r
i
t
t
e
n
a
s
:
x
G
r
e
a
t
T
h
a
n
(
x
,
1
)
CS411: Artificial Intelligence I, Bing Liu
8
Universe of Discourse
The
universe of discourse
, also called
universe
(also called
domain
), is the set of objects of interest.
Universal Quantifier (
): The expression:
x P(x)
,
denotes the
universal quantification of
P
(x).
In English: "
For all x, P(x)
holds" or "
for every x, P(x)
holds".
P(x)
is true for every object
x
in the universe
Existential Quantifier(
): The expression:
xP(x)
,
denotes the
existential quantification of
P(x)
.
In English: "There exists an
x
such that
P(x)
" or "There is at least one
x
such that
P(x)
“.
x
means at least one object
x
in the universe.
CS411: Artificial Intelligence I, Bing Liu
9
Application of Quantifiers
When more than one variable is quantified in a wff such
as
y
x P
(
x, y
),
they are applied from the inside
i.e., the one closest to the atomic formula is applied first. Thus
y
x P
(
x, y
),
reads
y
[
x P
(
x, y
)]
Some properties
T
h
e
p
o
s
i
t
i
o
n
s
o
f
d
i
f
f
e
r
e
n
t
t
y
p
e
s
o
f
q
u
a
n
t
i
f
i
e
r
s
c
a
n
n
o
t
b
e
s
w
i
t
c
h
e
d
.
F
o
r
e
x
a
m
p
l
e
,
x
y
P
(
x
,
y
)
i
s
n
o
t
e
q
u
i
v
a
l
e
n
t
t
o
y
x
P
(
x
,
y
)
.
¬
∀
x
P
(
x
)
equivalent to
∃
x ¬
P
(
x
)
CS411: Artificial Intelligence I, Bing Liu
10
Examples
Let P(x, y) stands for “x likes y”.
(
1
)
.
x
y
P
(
x
,
y
)
:
T
h
e
r
e
i
s
a
p
e
r
s
o
n
w
h
o
l
i
k
e
s
e
v
e
r
y
p
e
r
s
o
n
.
(
2
)
.
y
x
P
(
x
,
y
)
:
F
o
r
a
n
y
p
e
r
s
o
n
y
,
t
h
e
r
e
i
s
a
p
e
r
s
o
n
x
w
h
o
l
i
k
e
s
y
.
Let P(x, y) stands for “x < y”.
(
1
)
.
x
y
P
(
x
,
y
)
:
T
h
e
r
e
i
s
a
n
u
m
b
e
r
x
t
h
a
t
i
s
s
m
a
l
l
e
r
t
h
a
n
a
n
y
n
u
m
b
e
r
y
.
(
2
)
.
y
x
P
(
x
,
y
)
:
F
o
r
a
n
y
n
u
m
b
e
r
,
t
h
e
r
e
i
s
a
s
m
a
l
l
e
r
n
u
m
b
e
r
CS411: Artificial Intelligence I, Bing Liu
11
How to read
quantified formulas
L
e
t
F
(
x
,
y
)
s
t
a
n
d
s
f
o
r
“
x
f
l
i
e
s
f
a
s
t
e
r
t
h
a
n
y
”
.
l
e
t
t
h
e
u
n
i
v
e
r
s
e
b
e
t
h
e
s
e
t
o
f
a
i
r
p
l
a
n
e
s
.
x
y
F
(
x
,
y
)
:
"
F
o
r
e
v
e
r
y
a
i
r
p
l
a
n
e
x
t
h
e
f
o
l
l
o
w
i
n
g
h
o
l
d
s
:
x
i
s
f
a
s
t
e
r
t
h
a
n
a
n
y
a
i
r
p
l
a
n
e
y
"
.
O
r
s
i
m
p
l
y
:
"
E
v
e
r
y
a
i
r
p
l
a
n
e
i
s
f
a
s
t
e
r
t
h
a
n
e
v
e
r
y
a
i
r
p
l
a
n
e
(
i
n
c
l
u
d
i
n
g
i
t
s
e
l
f
!
)
"
.
x
y
F
(
x
,
y
)
:
"
F
o
r
e
v
e
r
y
a
i
r
p
l
a
n
e
x
t
h
e
f
o
l
l
o
w
i
n
g
h
o
l
d
s
:
f
o
r
s
o
m
e
a
i
r
p
l
a
n
e
y
,
x
i
s
f
a
s
t
e
r
t
h
a
n
y
"
.
O
r
s
i
m
p
l
y
:
"
E
v
e
r
y
a
i
r
p
l
a
n
e
i
s
f
a
s
t
e
r
t
h
a
n
s
o
m
e
a
i
r
p
l
a
n
e
"
.
x
y
F
(
x
,
y
)
:
"
T
h
e
r
e
e
x
i
s
t
a
n
a
i
r
p
l
a
n
e
x
w
h
i
c
h
s
a
t
i
s
f
i
e
s
t
h
e
f
o
l
l
o
w
i
n
g
:
(
o
r
s
u
c
h
t
h
a
t
)
f
o
r
e
v
e
r
y
a
i
r
p
l
a
n
e
y
,
x
i
s
f
a
s
t
e
r
t
h
a
n
y
"
.
O
r
s
i
m
p
l
y
:
“
s
o
m
e
a
i
r
p
l
a
n
e
i
s
f
a
s
t
e
r
t
h
a
n
e
v
e
r
y
a
i
r
p
l
a
n
e
"
.
x
y
F
(
x
,
y
)
:
"
F
o
r
s
o
m
e
a
i
r
p
l
a
n
e
x
t
h
e
r
e
e
x
i
s
t
s
a
n
a
i
r
p
l
a
n
e
y
s
u
c
h
t
h
a
t
x
i
s
f
a
s
t
e
r
t
h
a
n
y
“
.
O
r
s
i
m
p
l
y
:
"
S
o
m
e
a
i
r
p
l
a
n
e
i
s
f
a
s
t
e
r
t
h
a
n
s
o
m
e
a
i
r
p
l
a
n
e
"
.
CS411: Artificial Intelligence I, Bing Liu
12
Well-Formed Formula (wff)
W
f
f
s
(
o
r
s
e
n
t
e
n
c
e
s
)
a
r
e
c
o
n
s
t
r
u
c
t
e
d
u
s
i
n
g
t
h
e
f
o
l
l
o
w
i
n
g
r
u
l
e
s
:
True
and
False
are wffs.
Each propositional constant (i.e., specific proposition), and each
propositional variable (i.e., a variable representing propositions) are
wffs.
Each atomic formula (i.e. a specific predicate with variables) is a wff.
If
A
and
B
are wffs, then so are
A
, (
A
B
), (
A
B)
,
(A
B),
and
(A
B)
.
If
x
is a variable (representing objects of the universe of discourse),
and
A
is a wff, then so are
x A
and
x A
.
CS411: Artificial Intelligence I, Bing Liu
13
Some examples of first-order logic
There is some course that every student has taken.
∃
y Course(y)
∧
[
∀
x Student(x) → Takes(x, y)]
Every even integer greater than 2 is the sum of two primes.
∀
x EvenInt(x)
∧
Greater(x, 2) →
∃
y
∃
z Equals(x, Sum(y, z))
∧
Prime(y)
∧
Prime(z)
If a student takes a course and the course covers a concept,
then the student knows that concept.
∀
x
∀
y
∀
z (Student(x)
∧
Takes(x, y)
∧
Course(y)
∧
Covers(y, z)) → Knows(x, z)
CS411: Artificial Intelligence I, Bing Liu
14
Outline
Syntax
Semantics
Inference based on modus ponens
Inference based on classic reasoning
Summary
15
CS411: Artificial Intelligence I, Bing Liu
Models in first-order logic
A model
w
in first-order logic maps:
constant symbols to objects
w(Alice) = o
1
, w(Bob) = o
2
, w(Arithmetic) = o
3
predicate symbols to tuples of objects
w(Knows) = {(o1
, o
3
), (o
2
, o
3
), . . . }
Unique names assumption
:
Each object has at most one constant symbol.
Domain closure:
Each object has at least one constant symbol.
CS411: Artificial Intelligence I, Bing Liu
16
Propositionalization
If one-to-one mapping between constant symbols and objects:
(unique names –
only one name for an object
; domain closure
– at least one name
),
first-order logic is syntactic sugar for propositional logic
E.g., Knowledge base in first-order logic
Student(alice)
∧
Student(bob)
∀
x Student(x) → Person(x)
∃
x Student(x)
∧
Creative(x)
Knowledge base in propositional logic
Studentalice
∧
Studentbob
(Studentalice → Personalice)
∧
(Studentbob → Personbob)
(Studentalice
∧
Creativealice)
∨
(Studentbob
∧
Creativebob)
CS411: Artificial Intelligence I, Bing Liu
17
We can use any
inference algorithm
for propositional
logic!
Outline
Syntax
Semantics
Inference based on modus ponens
Inference based on classic reasoning
Summary
18
CS411: Artificial Intelligence I, Bing Liu
Definite clauses
D
e
f
i
n
i
t
e
c
l
a
u
s
e
(
f
i
r
s
t
-
o
r
d
e
r
l
o
g
i
c
)
A definite clause has the following form:
∀
x
1
· · ·
∀
x
n
(a
1
∧
· · ·
∧
a
k
) → b
for variables x
1
, . . . , x
n
and atomic formulas a
1
, . . . , a
k
, b (which
contain those variables).
For example,
∀
x
∀
y
∀
z (Takes(x, y)
∧
Covers(y, z)) → Knows(x, z)
CS411: Artificial Intelligence I, Bing Liu
19
Modus ponens (first attempt)
Definition:
modus ponens
(first-order logic)
a
1
, . . . , a
k
∀
x
1
· · ·
∀
x
n
(
a
1
∧
· · ·
∧
a
k
) → b
b
Example: Given P(Alice) and
∀
x P(x) → Q(x).
We cannot use the above modus ponens because P(Alice) and P(x)
do not match.
We need
substitution
and
unification
CS411: Artificial Intelligence I, Bing Liu
20
Substitution
Subst[{x/Alice}, P(x)] = P(Alice)
Subst[{x/Alice, y/z}, P(x) ∧
K(x, y)] = P(Alice)
∧
K(Alice, z)
Definition:
Substitution
A substitution
θ
is a mapping from variables to terms. Subst[
θ
,
f
]
returns the result of performing substitution
θ
on
f
.
CS411: Artificial Intelligence I, Bing Liu
21
Unification
Unify[Knows(Alice, Arithmetic), Knows(x, Arithmetic)] = {x/Alice}
Unify[Knows(Alice, y), Knows(x, z)] = {x/Alice, y/z}
Unify[Knows(Alice, y),Knows(Bob, z)] = fail
Unify[Knows(Alice, y),Knows(x, F(x))] = {x/Alice, y/F(Alice)}
Definition:
Unification
Unification takes two formulas
f
and
g
and returns a substitution
θ
which is
the most general unifier: Unify[
f
,
g
] =
θ
such that Subst[
θ
,
f
] = Subst[
θ
,
g
] or
”fail” if no such
θ
exists.
CS411: Artificial Intelligence I, Bing Liu
22
Modus ponens
Definition:
modus ponens
(first-order logic)
a’
1
, . . . , a’
k
∀
x
1
· · ·
∀
x
k
(a
1
∧
· · ·
∧
a
k
) → b
b’
Get most general unifier
θ
on premises:
θ =
Unify[a’
1
, . . . , a’
k
, a
1
∧
· · ·
∧
a
k
]
Apply
θ
to conclusion:
Subst[
θ,
b] = b’
CS411: Artificial Intelligence I, Bing Liu
23
Modus ponens example
Premises:
Takes(Alice, CS411)
Covers(CS411, Logic)
∀
x
∀
y
∀
z Takes(x, y)
∧
Covers(y, z) → Knows(x, z)
Conclusion:
θ = {x/Alice, y/CS411, z/Logic}
Derive Knows(Alice, Logic)
CS411: Artificial Intelligence I, Bing Liu
24
Completeness and semi-decidability
Theorem:
completeness
Modus ponens is complete for first-order logic with only Horn clauses.
Theorem:
semi-decidability
First-order logic (even restricted to only Horn clauses) is semi-decidable.
If KB |=
f
, forward inference on complete inference rules will prove
f
in finite time.
If KB |=/
f
, no algorithm can show this in finite time.
CS411: Artificial Intelligence I, Bing Liu
25
Resolution
First-order logic includes non-Horn clauses
∀
x Student(x) →
∃
y Know(x, y)
Resolution (same as in propositional logic):
Convert all formulas to CNF (conjunctive normal form)
more complex than in propositional logic.
Repeatedly apply resolution rule
CS411: Artificial Intelligence I, Bing Liu
26
Conversion to CNF
Input:
Anyone who likes all animals is liked by someone
Output
New to first-order logic
All variables (e.g.,
x
) have universal quantifiers by default
I
n
t
r
o
d
u
c
e
S
k
o
l
e
m
f
u
n
c
t
i
o
n
s
(
e
.
g
.
,
Y
(
x
)
)
t
o
r
e
p
r
e
s
e
n
t
e
x
i
s
t
e
n
t
i
a
l
q
u
a
n
t
i
f
i
e
d
v
a
r
i
a
b
l
e
s
.
CS411: Artificial Intelligence I, Bing Liu
27
Conversion to CNF (cont.)
CS411: Artificial Intelligence I, Bing Liu
28
Conversion to CNF (cont.)
CS411: Artificial Intelligence I, Bing Liu
29
Resolution of first-order logic
D
e
f
i
n
i
t
i
o
n
:
r
e
s
o
l
u
t
i
o
n
r
u
l
e
(
f
i
r
s
t
-
o
r
d
e
r
l
o
g
i
c
)
Example
CS411: Artificial Intelligence I, Bing Liu
30
Outline
Syntax
Semantics
Inference based on modus ponens
Inference based on classic reasoning
Summary
31
CS411: Artificial Intelligence I, Bing Liu
Bound and free variables
A
v
a
r
i
a
b
l
e
i
n
a
w
f
f
i
s
s
a
i
d
t
o
b
e
b
o
u
n
d
i
f
e
i
t
h
e
r
a
s
p
e
c
i
f
i
c
v
a
l
u
e
i
s
a
s
s
i
g
n
e
d
t
o
i
t
o
r
i
t
i
s
q
u
a
n
t
i
f
i
e
d
.
I
f
a
n
a
p
p
e
a
r
a
n
c
e
o
f
a
v
a
r
i
a
b
l
e
i
s
n
o
t
b
o
u
n
d
,
i
t
i
s
c
a
l
l
e
d
f
r
e
e
.
T
h
e
e
x
t
e
n
t
o
f
t
h
e
a
p
p
l
i
c
a
t
i
o
n
(
e
f
f
e
c
t
)
o
f
a
q
u
a
n
t
i
f
i
e
r
,
c
a
l
l
e
d
t
h
e
s
c
o
p
e
o
f
t
h
e
q
u
a
n
t
i
f
i
e
r
,
i
s
i
n
d
i
c
a
t
e
d
b
y
s
q
u
a
r
e
b
r
a
c
k
e
t
s
[
]
.
If there are no square brackets, then the scope is understood to be the
smallest wff following the quantification.
F
o
r
e
x
a
m
p
l
e
,
i
n
x
P
(
x
,
y
)
,
The variable
x
is bound while
y
is free.
In
x
[
y P
(
x, y
)
Q
(
x, y
)]
,
x
and
y
in
P
(
x, y
) are bound, while
y
in
Q
(
x, y
) is free, because the scope of
y
is
P
(
x, y
). The scope of
x
is [
y P
(
x, y
)
Q
(
x, y
)] .
CS411: Artificial Intelligence I, Bing Liu
32
From Wff to Proposition
A wff is, in general, not a proposition.
For example, consider the wff
x P
(
x
), where
P
(
x
) means
x
0.
If the universe is
{1, 2, 3, 4, 5, 6}or any subset of natural numbers, the wff
is true.
But if the universe is {-2, -3, 5}, then it is not true.
Also,
x Q
(
x, y
),
where
Q
(
x, y
)
means
x
> y
for the universe
{1, 3,
5
}
may be true or false depending on the value of
y
.
T
h
e
s
p
e
c
i
f
i
c
a
t
i
o
n
o
f
t
h
e
u
n
i
v
e
r
s
e
a
n
d
a
n
a
s
s
i
g
n
m
e
n
t
o
f
a
v
a
l
u
e
t
o
e
a
c
h
f
r
e
e
v
a
r
i
a
b
l
e
i
n
a
w
f
f
i
s
c
a
l
l
e
d
a
n
i
n
t
e
r
p
r
e
t
a
t
i
o
n
f
o
r
t
h
e
w
f
f
.
CS411: Artificial Intelligence I, Bing Liu
33
Satisfiability
A
w
f
f
i
s
s
a
i
d
t
o
b
e
s
a
t
i
s
f
i
a
b
l
e
i
f
t
h
e
r
e
e
x
i
s
t
s
a
n
i
n
t
e
r
p
r
e
t
a
t
i
o
n
t
h
a
t
m
a
k
e
s
i
t
t
r
u
e
,
I.e., if there are a universe and an assignment of values to its free
variables that make the wff true.
A
w
f
f
i
s
c
a
l
l
e
d
u
n
s
a
t
i
s
f
i
a
b
l
e
,
i
f
t
h
e
r
e
i
s
n
o
i
n
t
e
r
p
r
e
t
a
t
i
o
n
t
h
a
t
m
a
k
e
s
i
t
t
r
u
e
.
E.g.:
x P
(
x
), where
P
(
x
) means
x
0, is satisfiable, if our
universe is
{1, 2, 3, 4, 5, 6}.
x
[
P
(
x
)
P(x)] is not satisfiable.
CS411: Artificial Intelligence I, Bing Liu
34
Validity
A
w
f
f
i
s
v
a
l
i
d
i
f
i
t
i
s
t
r
u
e
f
o
r
e
v
e
r
y
i
n
t
e
r
p
r
e
t
a
t
i
o
n
.
E
.
g
.
,
t
h
e
w
f
f
x
P
(
x
)
x
P
(
x
)
i
s
v
a
l
i
d
f
o
r
a
n
y
p
r
e
d
i
c
a
t
e
n
a
m
e
P
,
b
e
c
a
u
s
e
x
P
(
x
)
i
s
t
h
e
n
e
g
a
t
i
o
n
o
f
x
P
(
x
)
.
Validity is analogue to tautology.
E.g., the wff
x P
(
x
)
is satisfiable but not valid.
CS411: Artificial Intelligence I, Bing Liu
35
Reasoning with first-order logic
Predicate logic is more powerful than propositional logic as it
allows one to reason about properties and relationships of
individual objects.
I
n
p
r
e
d
i
c
a
t
e
l
o
g
i
c
,
o
n
e
c
a
n
u
s
e
s
o
m
e
a
d
d
i
t
i
o
n
a
l
i
n
f
e
r
e
n
c
e
r
u
l
e
s
,
a
s
w
e
l
l
a
s
t
h
o
s
e
f
o
r
p
r
o
p
o
s
i
t
i
o
n
a
l
l
o
g
i
c
.
Inference rules of predicate logic
universal instantiation
universal generalization
existential instantiation
existential generalization
CS411: Artificial Intelligence I, Bing Liu
36
Universal Instantiation
x P(x)
----------
P(c)
where
c
is some arbitrary element of the universe.
For example, the following argument can be proven correct using the Universal Instantiation:
"
No humans can fly. Tom is human. Therefore, Tom cannot fly."
The argument is
[
x [Human(x)
Fly(x)]
Human(Tom) ]
Fly(Tom).
The proof is
1.
x [Human(x)
Fly(x)]
Hypothesis
2.
Human(Tom)
Hypothesis
3.
Human(Tom)
Fly(Tom)
Universal instantiation on 1.
4.
Fly(Tom)
Modus ponens on 2 and 3.
CS411: Artificial Intelligence I, Bing Liu
37
Universal Generalization
P(c)
----------
x P(x)
where
P(c)
holds for every element c of the universe of discourse.
For every number x if x > 1, then x - 1 > 0. Also for every number x, x > 1. We conclude that
for every number x, x - 1 >0.
Then the argument above is represented by (
P(x): x > 1; Q(x): x - 1> 0
)
[
x[P(x)
Q(x)]
x P(x)]
x Q(x)
To prove it we proceed as follows:
1.
x [P(x)
Q(x)]
Hypothesis
2.
x P(x)
Hypothesis
3.
[P(x)
Q(x)]
Universal Instantiation on 1.
4.
P(x) for the same x as in 3.
Universal Instantiation on 2.
5.
Q(x)
Modus ponens on 3 and 4.
6.
x Q(x)
Universal Generalization on 5
CS411: Artificial Intelligence I, Bing Liu
38
Existential Instantiation
x P(x)
-------
P(c)
where
c
is some element of the universe of discourse. It is not arbitrary but
must be one for which P(c) is true.
If you get 95 on the final exam for CS411, then you get an A for the course. Someone, say s,
gets 95 on the final exam. Therefore, s gets an A for CS411.
Let the universe be the set of all people in the world, let G(x) mean that x gets 95 on the final
exam of CS411, and let A(x) represent that x gets an A for CS411
.
Then the proof proceeds as follows:
1.
x [G(x)
A(x)]
Hypothesis
2.
x G(x)
Hypothesis
3.
G(s)
Existential instantiation on 3.
4.
G(s)
A(s)
Universal instantiation on 1.
5.
A(s)
Modus ponens on 3 and 4.
CS411: Artificial Intelligence I, Bing Liu
39
Existential Generalization
P(c)
----------
x P(x)
where
c
is an element of the universe.
"if everyone is happy then someone is happy"
To prove it, first let the universe be the set of all people and
let
Happy(x)
mean that x is happy
.
Then the argument is
x Happy(x)
x Happy(x)
The proof is
1.
x Happy(x)
Hypothesis
2.
Happy(c)
Universal instantiation
3.
x Happy(x)
Existential generalization.
CS411: Artificial Intelligence I, Bing Liu
40
Outline
Syntax
Semantics
Inference based on modus ponens
Inference based on classic reasoning
Summary
41
CS411: Artificial Intelligence I, Bing Liu
Summary
First-order logic (FOL) is a very expressive formal language
as variables yield very compact knowledge representations.
Many domains of technical knowledge can be written in FOL
(see AIMA Ch. 10)
circuits, software, planning, network and security protocols,
ecommerce transactions, knowledge graph, Semantic Web, etc.
Inference is semi-decidable in general; many problems are
efficiently solvable in practice.
CS411: Artificial Intelligence I, Bing Liu
42
Explore the limitations of propositional logic and delve into the syntax, semantics, and inference rules of first-order logic. Learn about predicates, quantification, and how to express relationships among objects using predicates. Enhance your understanding of how first-order logic provides a more expressive power compared to propositional logic.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
First-order Logic Some slides are borrowed from Chelsea Finn & Nima Anari
Limitations of propositional logic Propositional logic is rather limited in its expressive power. E.g., For every x, x > 0 is true if x is a positive integer. We cannot say it in propositional logic. Nor can we show the following logical equivalences: "Not all birds fly" is equivalent to "Some birds don't fly". "Not all integers are even" is equivalent to "Some integers are not even". "Not all cars are expensive" is equivalent to "Some cars are not expensive . We need first-order logic. 2 CS411: Artificial Intelligence I, Bing Liu
Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 3 CS411: Artificial Intelligence I, Bing Liu
Syntax of first-order logic Terms (refer to objects): Constant symbol (e.g., Arithmetic) starts with a capital letter Variable (e.g., x) Function of terms (e.g., Sum(3, x)) Formulas: Atomic formulas (atoms): predicate applied to terms (e.g., Knows(x, Arithmetic)) Connectives applied to formulas (e.g., Student(x) Knows(x, Arithmetic)) Quantifiers applied to formulas (e.g., x Student(x) Knows(x, Arithmetic)) 4 CS411: Artificial Intelligence I, Bing Liu
Predicate Predicate: A predicate is a property about of some objects or a relationship among objects represented by the variables. Example "The sky is blue "The cover of this book is blue" For the above two sentences, we can use is_Blue as the predicate. We can also simply use B. B(x), where x is variable representing an arbitrary object. B(x) reads as "x is blue". 5 CS411: Artificial Intelligence I, Bing Liu
Another predicate example "John gives the book to Mary", "Jim gives a loaf of bread to Tom", and "Jane give a lecture to Mary" All can be expressed using this predicate: Give(x, y, z) which reads, x gives y to z. E.g., Give(John, Book, Mary), Give(Jane, Lecture, Mary) 6 CS411: Artificial Intelligence I, Bing Liu
Quantification A predicate with variables is not a proposition (with truth value of T or F). E.g., the statement x > 1 with variable x over the universe of real numbers is neither true nor false since we don't know what x is. It can be true or false depending on the value of x. For x > 1 to be a proposition either we substitute a specific number for x, or change it to something like "There is a number x for which x > 1 holds", or "For every number x, x > 1 holds". We are using quantifiers. 7 CS411: Artificial Intelligence I, Bing Liu
From predicate to propositions A predicate with variables (called an atomic formula) can be made a proposition by applying one of the following two operations to each of its variables: assign a value to the variable quantify the variable using a quantifier Let us use predicate GreatThan(x, 1) to represent x >1. universal quantifier: for every object x in the universe, x > 1 written as: x GreatThan(x, 1) existential quantifier: "for some object x in the universe, x > 1 written as: x GreatThan(x, 1) 8 CS411: Artificial Intelligence I, Bing Liu
Universe of Discourse The universe of discourse, also called universe (also called domain), is the set of objects of interest. Universal Quantifier ( ): The expression: x P(x), denotes the universal quantification of P(x). In English: "For all x, P(x) holds" or "for every x, P(x) holds". P(x) is true for every object x in the universe Existential Quantifier( ): The expression: xP(x), denotes the existential quantification of P(x). In English: "There exists an x such that P(x)" or "There is at least one x such that P(x) . x means at least one object x in the universe. 9 CS411: Artificial Intelligence I, Bing Liu
Application of Quantifiers When more than one variable is quantified in a wff such as y x P(x, y), they are applied from the inside i.e., the one closest to the atomic formula is applied first. Thus y x P(x, y), reads y [ x P(x, y)] Some properties The positions of different types of quantifiers cannot be switched. For example, x y P(x, y ) is not equivalent to y x P(x, y ). x P(x) equivalent to x P(x) 10 CS411: Artificial Intelligence I, Bing Liu
Examples Let P(x, y) stands for x likes y . (1). x y P(x, y): There is a person who likes every person. (2). y x P(x, y): For any person y, there is a person x who likes y. Let P(x, y) stands for x < y . (1). x y P(x, y): There is a number x that is smaller than any number y. (2). y x P(x, y): For any number, there is a smaller number 11 CS411: Artificial Intelligence I, Bing Liu
How to read quantified formulas Let F(x, y) stands for x flies faster than y . let the universe be the set of airplanes. x yF(x, y): "For every airplane x the following holds: x is faster than any airplane y". Or simply: "Every airplane is faster than every airplane (including itself!)". x yF(x, y): "For every airplane x the following holds: for some airplane y, x is faster than y". Or simply: "Every airplane is faster than some airplane". x y F(x, y): "There exist an airplane x which satisfies the following: (or such that) for every airplane y, x is faster than y". Or simply: some airplane is faster than every airplane". x yF(x, y): "For some airplane x there exists an airplane y such that x is faster than y . Or simply: "Some airplane is faster than some airplane". 12 CS411: Artificial Intelligence I, Bing Liu
Well-Formed Formula (wff) Wffs (or sentences) are constructed using the following rules: True and False are wffs. Each propositional constant (i.e., specific proposition), and each propositional variable (i.e., a variable representing propositions) are wffs. Each atomic formula (i.e. a specific predicate with variables) is a wff. If A and B are wffs, then so are A, (A B), (A B), (A B), and (A B). If x is a variable (representing objects of the universe of discourse), and A is a wff, then so are x A and x A . 13 CS411: Artificial Intelligence I, Bing Liu
Some examples of first-order logic There is some course that every student has taken. y Course(y) [ x Student(x) Takes(x, y)] Every even integer greater than 2 is the sum of two primes. x EvenInt(x) Greater(x, 2) y z Equals(x, Sum(y, z)) Prime(y) Prime(z) If a student takes a course and the course covers a concept, then the student knows that concept. x y z (Student(x) Takes(x, y) Course(y) Covers(y, z)) Knows(x, z) 14 CS411: Artificial Intelligence I, Bing Liu
Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 15 CS411: Artificial Intelligence I, Bing Liu
Models in first-order logic A model w in first-order logic maps: constant symbols to objects w(Alice) = o1, w(Bob) = o2, w(Arithmetic) = o3 predicate symbols to tuples of objects w(Knows) = {(o1, o3), (o2, o3), . . . } Unique names assumption: Each object has at most one constant symbol. Domain closure: Each object has at least one constant symbol. 16 CS411: Artificial Intelligence I, Bing Liu
Propositionalization If one-to-one mapping between constant symbols and objects: (unique names only one name for an object; domain closure at least one name), first-order logic is syntactic sugar for propositional logic E.g., Knowledge base in first-order logic Student(alice) Student(bob) x Student(x) Person(x) x Student(x) Creative(x) Knowledge base in propositional logic Studentalice Studentbob (Studentalice Personalice) (Studentbob Personbob) (Studentalice Creativealice) (Studentbob Creativebob) We can use any inference algorithm for propositional logic! 17 CS411: Artificial Intelligence I, Bing Liu
Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 18 CS411: Artificial Intelligence I, Bing Liu
Definite clauses Definite clause (first-order logic) A definite clause has the following form: x1 xn (a1 ak) b for variables x1, . . . , xn and atomic formulas a1, . . . , ak, b (which contain those variables). For example, x y z (Takes(x, y) Covers(y, z)) Knows(x, z) 19 CS411: Artificial Intelligence I, Bing Liu
Modus ponens (first attempt) Definition: modus ponens (first-order logic) a1, . . . , ak x1 xn(a1 ak) b b Example: Given P(Alice) and x P(x) Q(x). We cannot use the above modus ponens because P(Alice) and P(x) do not match. We need substitution and unification 20 CS411: Artificial Intelligence I, Bing Liu
Substitution Subst[{x/Alice}, P(x)] = P(Alice) Subst[{x/Alice, y/z}, P(x) K(x, y)] = P(Alice) K(Alice, z) Definition: Substitution A substitution is a mapping from variables to terms. Subst[ , f] returns the result of performing substitution on f. 21 CS411: Artificial Intelligence I, Bing Liu
Unification Unify[Knows(Alice, Arithmetic), Knows(x, Arithmetic)] = {x/Alice} Unify[Knows(Alice, y), Knows(x, z)] = {x/Alice, y/z} Unify[Knows(Alice, y),Knows(Bob, z)] = fail Unify[Knows(Alice, y),Knows(x, F(x))] = {x/Alice, y/F(Alice)} Definition: Unification Unification takes two formulas f and g and returns a substitution which is the most general unifier: Unify[f, g] = such that Subst[ , f] = Subst[ , g] or fail if no such exists. 22 CS411: Artificial Intelligence I, Bing Liu
Modus ponens Definition: modus ponens (first-order logic) a 1 , . . . , a k x1 xk(a1 ak) b b Get most general unifier on premises: = Unify[a 1 , . . . , a k, a1 ak] Apply to conclusion: Subst[ , b] = b 23 CS411: Artificial Intelligence I, Bing Liu
Modus ponens example Premises: Takes(Alice, CS411) Covers(CS411, Logic) x y z Takes(x, y) Covers(y, z) Knows(x, z) Conclusion: = {x/Alice, y/CS411, z/Logic} Derive Knows(Alice, Logic) 24 CS411: Artificial Intelligence I, Bing Liu
Completeness and semi-decidability Theorem: completeness Modus ponens is complete for first-order logic with only Horn clauses. Theorem: semi-decidability First-order logic (even restricted to only Horn clauses) is semi-decidable. If KB |= f, forward inference on complete inference rules will prove f in finite time. If KB |=/ f, no algorithm can show this in finite time. 25 CS411: Artificial Intelligence I, Bing Liu
Resolution First-order logic includes non-Horn clauses x Student(x) y Know(x, y) Resolution (same as in propositional logic): Convert all formulas to CNF (conjunctive normal form) more complex than in propositional logic. Repeatedly apply resolution rule 26 CS411: Artificial Intelligence I, Bing Liu
Conversion to CNF Input: Anyone who likes all animals is liked by someone Output New to first-order logic All variables (e.g., x) have universal quantifiers by default Introduce Skolem functions (e.g., Y(x)) to represent existential quantified variables. 27 CS411: Artificial Intelligence I, Bing Liu
Conversion to CNF (cont.) 28 CS411: Artificial Intelligence I, Bing Liu
Conversion to CNF (cont.) 29 CS411: Artificial Intelligence I, Bing Liu
Resolution of first-order logic Definition: resolution rule (first-order logic) Example 30 CS411: Artificial Intelligence I, Bing Liu
Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 31 CS411: Artificial Intelligence I, Bing Liu
Bound and free variables A variable in a wff is said to be bound if either a specific value is assigned to it or it is quantified. If an appearance of a variable is not bound, it is called free. The extent of the application (effect) of a quantifier, called the scope of the quantifier, is indicated by square brackets [ ]. If there are no square brackets, then the scope is understood to be the smallest wff following the quantification. For example, in x P(x, y), The variable x is bound while y is free. In x [ y P(x, y) Q(x, y)], x and y in P(x, y) are bound, while y in Q(x, y) is free, because the scope of y is P(x, y). The scope of x is [ y P(x, y) Q(x, y)] . 32 CS411: Artificial Intelligence I, Bing Liu
From Wff to Proposition A wff is, in general, not a proposition. For example, consider the wff x P(x), where P(x) means x 0. If the universe is {1, 2, 3, 4, 5, 6} or any subset of natural numbers, the wff is true. But if the universe is {-2, -3, 5}, then it is not true. Also, x Q(x, y), where Q(x, y) means x > y for the universe {1, 3, 5} may be true or false depending on the value of y. The specification of the universe and an assignment of a value to each free variable in a wff is called an interpretation for the wff. 33 CS411: Artificial Intelligence I, Bing Liu
Satisfiability A wff is said to be satisfiable if there exists an interpretation that makes it true, I.e., if there are a universe and an assignment of values to its free variables that make the wff true. A wff is called unsatisfiable, if there is no interpretation that makes it true. E.g.: x P(x), where P(x) means x 0, is satisfiable, if our universe is {1, 2, 3, 4, 5, 6}. x [P(x) P(x)] is not satisfiable. 34 CS411: Artificial Intelligence I, Bing Liu
Validity A wff is valid if it is true for every interpretation. E.g., the wff x P(x) x P(x)is valid for any predicate name P , because x P(x)is the negation of x P(x). Validity is analogue to tautology. E.g., the wff x P(x) is satisfiable but not valid. 35 CS411: Artificial Intelligence I, Bing Liu
Reasoning with first-order logic Predicate logic is more powerful than propositional logic as it allows one to reason about properties and relationships of individual objects. In predicate logic, one can use some additional inference rules, as well as those for propositional logic. Inference rules of predicate logic universal instantiation universal generalization existential instantiation existential generalization 36 CS411: Artificial Intelligence I, Bing Liu
Universal Instantiation x P(x) ---------- P(c) where c is some arbitrary element of the universe. For example, the following argument can be proven correct using the Universal Instantiation: "No humans can fly. Tom is human. Therefore, Tom cannot fly." The argument is [ x [Human(x) Fly(x)] Human(Tom) ] Fly(Tom). The proof is 1. x [Human(x) Fly(x)] 2. Human(Tom) 3. Human(Tom) Fly(Tom) 4. Fly(Tom) Hypothesis Hypothesis Universal instantiation on 1. Modus ponens on 2 and 3. 37 CS411: Artificial Intelligence I, Bing Liu
Universal Generalization P(c) ---------- x P(x) where P(c) holds for every element c of the universe of discourse. For every number x if x > 1, then x - 1 > 0. Also for every number x, x > 1. We conclude that for every number x, x - 1 >0. Then the argument above is represented by (P(x): x > 1; Q(x): x - 1> 0) [ x[P(x) Q(x)] x P(x)] x Q(x) To prove it we proceed as follows: 1. x [P(x) Q(x)] 2. x P(x) 3. [P(x) Q(x)] 4. P(x) for the same x as in 3. 5. Q(x) 6. x Q(x) Hypothesis Hypothesis Universal Instantiation on 1. Universal Instantiation on 2. Modus ponens on 3 and 4. Universal Generalization on 5 38 CS411: Artificial Intelligence I, Bing Liu
Existential Instantiation x P(x) ------- P(c) where c is some element of the universe of discourse. It is not arbitrary but must be one for which P(c) is true. If you get 95 on the final exam for CS411, then you get an A for the course. Someone, say s, gets 95 on the final exam. Therefore, s gets an A for CS411. Let the universe be the set of all people in the world, let G(x) mean that x gets 95 on the final exam of CS411, and let A(x) represent that x gets an A for CS411. Then the proof proceeds as follows: 1. x [G(x) A(x)] Hypothesis 2. x G(x) Hypothesis 3. G(s) Existential instantiation on 3. 4. G(s) A(s) Universal instantiation on 1. 5. A(s) Modus ponens on 3 and 4. 39 CS411: Artificial Intelligence I, Bing Liu
Existential Generalization P(c) ---------- x P(x) where c is an element of the universe. "if everyone is happy then someone is happy" To prove it, first let the universe be the set of all people and let Happy(x) mean that x is happy. Then the argument is x Happy(x) x Happy(x) The proof is 1. x Happy(x) Hypothesis 2. Happy(c) Universal instantiation 3. x Happy(x) Existential generalization. 40 CS411: Artificial Intelligence I, Bing Liu
Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 41 CS411: Artificial Intelligence I, Bing Liu
Summary First-order logic (FOL) is a very expressive formal language as variables yield very compact knowledge representations. Many domains of technical knowledge can be written in FOL (see AIMA Ch. 10) circuits, software, planning, network and security protocols, ecommerce transactions, knowledge graph, Semantic Web, etc. Inference is semi-decidable in general; many problems are efficiently solvable in practice. 42 CS411: Artificial Intelligence I, Bing Liu
