Transcript First Order Logic and Resolution

Lecture 8: First Order Logic
Heshaam Faili
[email protected]
University of Tehran
Motivation for First Order
Logic (FOL)
FOL syntax
Quantifiers
FOL semantics
Building KB in FOL
Inference rules for FOL
History



First Order Logic (FOL) was essentially
developed by Gottlob Frege around
1879.
The goal was to create a sound and
complete system from which all logical
truths could be derived.
In 1930, Kurt Godel showed that such a
system does not exist (Godel’s
completeness theorem).
2
Formal languages
Natural
Language like English, Persian
Properties:
-Declarative
Are more expressive languages
Compositionality
-But involve a lot of ambiguity
-Used for communication rather than
presentation
3
First-order logic -- rationale (1)

Extended language to express general
statements of the form:
“every person has a father and a mother”

without explicitly listing all instances
The extension requires:




variables: X, Y, … that can refer to specific objects
relations: father(X,Y), mother(Z,Y)
quantifiers: for all , there exists,  to specify the
scope of the variables
X Y Z father(Y,X) and mother(Z,X)
syntax, semantics, and deduction rules
4
First order logic -- rationale (2)



First order logic (FOL) and its properties have been
widely studied in Mathematics and Logic
FOL can express anything that can be programmed
Issues for knowledge representation:


how to effectively represent the world -- many ontologies
possible  KB design.
how to make sound, complete, and computationally
effective deductions with it.
5
Elements of First Order Logic (1)
Terms are primitive objects: they are built out of individual
variables and function symbols (and individual constants).
 individual constants: name of a single object in the world:
sarah, 55, blue
(True, False)
 individual variables: place holder for objects:
X, Y

function symbols: they are just symbols but will be
interpreted as operations on objects -- return an object
father(sarah), father(X), color(block), sarah(),
father(block)
6
Elements of First Order Logic (2)
Predicate symbols will be interpreted as relations
between objects: they act on terms
father_of 2-place father_of(sarah, moshe)
color_of
color
bird
2-place color_of(block123, blue),
1-place color(blue)
1-place bird(Tweety)
Functions: father(sarah) = moshe
Atomic formula
7
Elements of First Order Logic (3)
Formulas are built out of atomic formulas with
propositional connectives (, , ~, =>, <=>) and
quantifiers:  (universal) and  (existential):
father_of(sarah, husband(tal))
father(sarah) = husband(tal)
( X = father(sarah) )  (X = husband(tal))
 X (X = father(sarah) => X = moshe)
 X  Y father_of(X, Y)
 Y  X father_of(X, Y)
8
Elements of First Order Logic (4)


A sentence is a formula in which all
variables are quantified (no free variable)
KB is a set of sentences
on(a,b)  on(b,c)
clear(a)
color_of(a, blue)
a
b
c
9
FOL Example
10
First Order Logic -- Syntax
Formula
----> Atomic_Formula |
Formula Connective Formula |
Quantifier Variable Formula |
(Formula) | ~Formula
Atomic_Formula ----> PredicateS( Term, ..., Term) |
Term = Term
Term
----> Constant | Variable |
FunctionS( Term, …, Term)
Connective
---->  |  | => | <=>
Quantifier
---->  | 
Constant
----> sara, 55, blue,... (lower case letters)
Variable
-----> X, Y, ….
(upper case letters)
PredicateS
----> before(_,_) …. (n-ary relation)
11
FunctionS
----> mother(_,_), >, ..(n-ary function)
Terminology




A literal is an atomic formula or its negation
A clause is a disjunction of literals
A term without variables is called a ground
term.
A clause without variables is called a ground
clause
father_of(sarah, moshe)

 father (lea, moshe)
Our convention:


ground terms start with lower case letters
uninstantiated variables start with capital letters
12
Universal Quantifier

States that a sentence is true for all objects in the world
being modeled.
 X ( block(X) => color_of(X,red))
is used to claim that every object in the world that is a
block is red.
 X (X = a  X = b  X = c ) says that there are at most three
objects in the world and that they are denoted by a, b, c.
It is only in such a world that  X ( block(X) => color_of(X,red)) is
equivalent to:
block(a) => color_of(a,red)  block(b) => color_of(b,red) 
block(c) => color_of(c,red)
13
Existential Quantifier

States that a sentence is true for some objects in
the world being modeled.
 X block(X)  color_of(X,red)
is
equivalent to
block(a)  color_of(a,red) 
block(b)  color_of(b,red) 
block(c)  color_of(c,red)
in a world with at most three objects named by
a,b,c. Otherwise there may be a red block that is
not a, b or c.
14
Expressiveness

How can we say that the only objects in the
world are a, b and c?
X (X = a)  (X = b)  (X = c)
What is this?
~(a = b)  ~(a = c)  ~(b = c) ?
15
Quantifiers scope


Scope: in X S the scope of the quantifier is the
whole formula S.
X [block(X) => color_of(X,red)]  on(a,Y)
Order: existential quantifiers commute and
universal quantifiers commute
X (Y (Sentence)) equivalent to Y (X (Sentence))
X (Y(Sentence)) equivalent toY(X (Sentence))

Mixed quantifiers do NOT commute
X Y loves(X,Y) vs. Y X loves(X,Y)
everybody loves somebody vs.
somebody is loved by everybody
16
Relations between quantifiers


Existential and universal quantifiers are related
to each other through negation
DeMorgan’s laws for quantifiers
X ~P  ~ X P
~P  ~ Q  ~(P  Q)
~X P  X ~ P
X P  ~X ~ P
X P  ~ X ~ P

~(P Q)  ~P  ~Q
P Q  ~(~P  ~Q)
P  Q  ~ (~P ~Q)
Example:
every person has a father
there is no person that does not have a father
17
Equality and its use

The equality symbol indicates that two terms
refer to the same object
father(sarah) = moshe

indicates that the object refered to by
father(sarah) and by moshe are the same
Equality can be viewed as the identity relation
=(sarah,sarah), …

Used to distinguish between objects
X Y sister_of(sarah, X)  sister(sarah, Y)  ~(X=Y) to
specify that sarah has two sisters (at least)
18
First Order Logic – Semantics (1)



We define the meaning of terms and formulas
in structures with the help of an assignment for
the individual variables.
A structure consists of a non-empty domain, A,
a suitable function: An  A for every n-place
function symbol of , a subset of An for every nplace predicate symbol.
An variable assignment associates an element
of A with each individual variable.
19
First Order Logic – Semantics (2)
Every term is interpreted as an element of the
domain A:
 individual variables using the variable
assignment
 complex terms by applying the function
corresponding to the function symbol to the
interpretations of the arguments.
20
First Order Logic – Semantics (3)



Truth value of formulas is defined recursively
from the truth value of atomic formulas, as in
Propositional Logic
Atomic formula: using the interpretation of the
predicate symbol and the interpretations of
the terms: father_of(sarah, moshe) is true iff
the pair < sarah, moshe > of interpretations is
in the interpretation father_of.
_father_of is a subset of A2
21
First Order Logic – Semantics (4)



Formulas such as A  B, A  B, ~A, A=>B are interpreted
as in propositional calculus
X S is true iff there is some element w of the
domain A, such that S gets the value True, when
one uses not the original variable assignment but
the modified assignment in which X gets
associated with w.
X S is true iff S gets the value true with all
variable assignments that differ from the original
one only in the value associated with X.
22
Natural Numbers
NatNum(0)
n NatNum(n)  NatNum(S(n))
n, 0S(n)
m,n mn  S(m)  S(n)
m NatNum(m)  +(0,m) = m
m,n NatNum(m) NatNum(n)  +(S(m),n) = S(+(m,n))
23
Variable assignment and satisfiability


A sentence S is satisfied by a variable
assignment U when the ground sentence
S[U] is valid
|= S[U]
for U ={X/a, Y/b, ….}
The satisfiability of logical sentences is
determined by the logical connective
|=(S1  S2  …  Sn)[U] iff
|= Si[U]
for all i = 1 .. n
|=(S1  S2  …  Sn)[U] iff
|= Si[U]
for some i = 1 .. n
24
Expressing knowledge in FOL



Given a world or domain, identify and
define constant objects, functions, and
relation predicates
Define relevant domain knowledge stated
informally in English as a set of FOL
sentences
KB usually has two types of statements


statements about the specific objects -statements about general relationships -axioms
25
Example: family relations domain

Objects: members of the family
Functions: father, mother
Relations: male, female, parent_of, sibling_of,

statements about the specific family


brother_of, sister_of, child_of, daughter_of,
son_of, spouse_of, wife_of, husband_of, ….
female(sarah), father(sarah) = moshe

statements about family relationships
 X  Y : (Z = father(X)  Z = mother(X) ) =>
sibling(X, Y)
26
Some family relationships rules

A mother is a female parent
 M C mother(M) = C <=>
female(C)  parent_of(M,C)

A grandparent is a parent of one’s parent
 G  C grandparent_of(G,C) <=>
P parent_of(G,P)  parent_of(P,C)

Parent and child are inverse relations
P C parent_of(P,C) <=> child_of(C,P)

A sibling is another child of one’s parents
X Y sibling_of(X,Y) <=>
X  Y  P parent_of(P,X)  parent_of(P,Y)
27
Inference in First Order Logic


As for propositional logic, will work only on
the syntactic form of the sentences
Extend the rules of propositional logic to
deal with quantifiers and variables. The
rules will deal with variable assignment,
using (syntactic) substitutions.
28
Inference Rules: examples (1)
From KB:
1. M C mother(C) = M <=>
female(M)

parent(M,C)
2. mother(sarah) = ruth
Deduce:
female(ruth)

parent(ruth,sarah)
29
Inference Rules: examples (2)
From KB =
1. X father_of(Y, X) 
~husband_of(mother(Y), X)
2. husband_of(mother(Y), Z)
Deduce: father_of(Y, Z)
From KB = {X F(Y, X)  ~H(M(Y), X)
H(M(Y), Z)}
Deduce: F(Y, Z)
30
Substitution



Substitution is a syntactic operation that takes a
formula and replaces a variable everywhere it
appears by a term.
Subst(,S) is the result of replacing the variables X, Y, ….
by the terms t1, t2, … respectively in a formula S. The
result is denoted S[ ].  ={X/t1, Y/t2, …}
For example
father_of(X, Y) [ X/sarah, Y/moshe ]
father_of(sarah, moshe)
is
Substitution is syntactic, variable assignment is
semantic.
31
Other rules: good and bad

Universal Elimination:
X S
for any t S[X/t]
X S
S

In particular:

Universal Introduction:
S
X S
If KB does not
mention the
variable X
32
FOL -- Inference Rules for
quantifiers

Substitution operation
Subst(,S) is the result of applying the variable
assignment  ={X/x, Y/y, …} to S, i.e, S[ ]

Universal and Existential Elimination
X 
Subst ({ X / x}, )
X 
Subst ({ X / x}, )
x doesnot appear in the whole KB: skolemization

Existential Introduction

X Subst ({ X / x}, )
33
Example of a proof
“It is a crime for an American to sell
weapons to hostile nations. North Korea is
an enemy of America, has some missiles,
and all of its missiles were sold to it by
Coronel West, who is American.”
Prove that Coronel West is a criminal!
34
Formalization
1. X,Y,Z american(X)  weapon(Y)  nation(Z) 
hostile(Z)  sells(X,Z,Y)  criminal(X)
2. X missile(X)  owns(nkorea,X)
3. X missile(X)  owns(nkorea,X)  sells(west,nkorea,X)
4. X missile(X)  weapon(X)
5. X enemy(X,america)  hostile(X)
6. american(west)
7. nation(nkorea)
8. enemy(nkorea,america)
9. nation(america)
35
Proof (1)
2. and Existential elimination
10.
missile(m)  owns(nkorea,m)
X/m
10. and And-Elimination
11.
12.
owns(nkorea,m)
missile(m)
4. And Universal Elimination
13.
missile(m) => weapon(m)
12, 13 and Modus Ponens
14.
X/m
weapon(m)
3 and Universal Elimination
15. missile(m)  owns(nkorea,m) => sells(west,nkorea,m)
36
Proof (2)
15, 10 and Modus Ponens
16. sells(west, nkorea,m)
1 and Universal Elimination (three times)
17. american(west)  weapon(m)  nation(nkorea) 
hostile(nkorea)  sells(west,nkorea,m) =>
criminal(west)
5 and Universal Elimination
18.
enemy(nkorea,america) => hostile(nkorea)
8, 18 and Modus Ponens
37
Proof (3)
19. hostile(nkorea)
6, 7, 14, 16, 19 and And-Introduction
20. american(west)  weapon(m) 
nation(nkorea) 
hostile(nkorea) 
sells(west,nkorea,m)
17, 20 and Modus Ponens
21. criminal(west)
38
FOL inferences



Soundness: Rules for propositional logic are
sound.
Godel proposed a system R and proved in 1931
that in FOL any sentence that logically follows
from a KB can be proven:
if KB |= S then KB |=R S
Robinson developed in 1965 a mechanizable
proof procedure based on resolution -- we will
study it in detail next.
39
knowledge engineering
process

knowledge engineer is someone who investigates a
particular domain, learns what concepts are important in
that domain, and creates a formal representation of the
objects and relations in the domain.
 Identify the task.
 Assemble the relevant knowledge (Knowledge acquisition)
 Decide on a vocabulary of predicates, functions, and
constants.
 Encode general knowledge about the domain.
 Encode a description of the specific problem instance.
 Pose queries to the inference procedure and get answers.
 Debug the knowledge base.
40
Main differences with propositional
logic



There are infinitely many possible
models: we cannot just enumerate all
the models to see whether a sentence is
satisfied in all models.
There still exist refutation-complete rules
Godel’s incompleteness theorem says
that we cannot hope for the application
of these rules to terminate always when
the formula C is not entailed by KB.
41
Key issues in developing an
effective inference procedure



Have as few inference rules as possible
to reduce the search’s branching factor
The complexity is still exponential in the
number of atomic sentences
More efficient procedures for restricted
forms of logic sentences (Horn clauses)
42
?
43