Transcript First-Order Logic - Columbia University

First-Order Logic
Reading: C. 8 and C. 9
Pente specifications handed back at end
of class
First-Order Logic: Outline



Expressing Information in first-order logic
An example
Inference in FOL
• Resolution theorem proving
• Production systems (forward chaining)
• Logic-based programming (backward chaining)
2
Characteristics of FOL

Declarative

Expressive

Compositionality
• Partial information
• Negation
3
Ontological Commitment

Propositional logic:
•
•

There are facts that either hold or do not hold in the
world
Logic constrains facts
First-order logic:
•
•
The world consists of objects and relations between
objects
Logic constrains allowable objects, properties of
objects, relations between objects
4
Ontological commitments of higher
order logics

Temporal logic
• Facts hold at particular times and those times are
ordered

Epistemological

• The agent believes a fact
• The agent does not believe it
• The agent has no opinion
Probabilistic
• Agents hold beliefs about facts
• Three possible states of knowledge
• Facts are true to different degrees (Truth value from 0 to
1)
5
Problems with propositional logic
6
7
Propositional Logic is lacking in
expressiveness

Cannot represent knowledge of complex
environments in a concise way
• E.g., Squares adjacent to pits are breezy

Need objects

Need relations

Need functions
• Squares, pits, Kathy
• Adjacent, breezy, smelly, know
• Father-of, mother-of
8
Syntax of FOL: basic elements







Constants: Vijay, Andrew, Sowmya
Predicates: knows, adjacent, >
Functions: Sqrt, father-of
Variables: x,y,a,b
Connectives: Λ,V,⌐,→,↔
Equality: =
Quantifiers: ,
9
Atomic Sentences



Atomic sentence = predicate (term1…termm)
or term1=term2
Term = function (term1, …, termm)
or constant or variable
E.g. know(Kathy,Sowmya), Adjacent (x,y),
father-of(Kathy) = Michael, Andrew, x
10
Complex Sentences

Complex sentences are made from
atomic sentences using connectives
⌐S, S1ΛS2, S1VS2, S1S2, S1S2

E.g., adjacent(x,y)  adjacent (y,x),
⌐knows(Nunzio, Michael),
11
Truth in First-order Logic




Sentences are true with respect to a model and an
interpretation
Model contains  1 objects (domain elements) and
relations among them
Interpretation specifies referents for
•
•
•
Constant symbols -> objects
Predicate symbols -> relations
Function symbols -> functional relations
An atomic sentence predicate (term1,…,termn) is true iff
the objects referred to by term1,…, termn are in the
relation referred to by predicate.
12
Universal quantification



<variables> <sentence>
Everyone at Columbia is smart:
x At(x,Columbia)  Smart(x)
x P is true in a model m iff P with x being
each possible object in the model
At (Leia, Columbia)  Smart(Leia)
At (Ryan, Columbia)  Smart (Ryan)
At (Archana, Columbia)  Smart (Archana)
At (Stanley, Columbia)  Smart (Stanley)
…..
13
A common mistake


Typically,  is the main connective used with 
Common mistake: using as the main connective
Λ
x At(x,Columbia) Λ Smart(x)
14
Existential Quantification




<variables> <sentence>
Someone at Columbia is smart
x At(x,Columbia) Smart(x)
 x P is true in a model m iff P with x being each possible
object in the model
Equivalent to the disjunction of instantiations of P
At (Leia, Columbia) Λ Smart(Leia)
V At (Ryan, Columbia) Λ  Smart (Ryan)
V At (Archana, Columbia) Λ  Smart (Archana)
V At (Stanley, Columbia) Λ  Smart (Stanley)
15
Another Common Mistake


Typically, Λ is the main connective with

Common mistake: using  as the main
connective
 x At(x,Columbia)  Smart(x)
16
Properties of Quantifiers




x y is the same y x
x  y is the same as  y  x
 x  y is not the same as  y  x
•
•
•
•
 x y Loves(x,y)
There is a person who loves everyone in the world
 y  x Loves(x,y)
Everyone is loved by someone.
Quantifier duality: each can be expressed using the other
 x Likes (x,Icecream) ⌐ x ⌐ Likes(x,IceCream)
 x Likes(x, Broccoli)
⌐ x ⌐ Likes(x,Broccoli)
17
Translation from English to FOL

A mother is a female parent

Andrew likes the problem of one of the
book exercises

?
18
Example

Family trees

What does the model look like?

What can we infer?
• Father-of
• Mother-of
• Sibling
• Cousin
• Ancestors
19
To Make Inferences in FOL

Method 1

Method 2
• Unification of variables with literals (in the KB)
• Generalized Modus Ponens
• Forward-chaining or Backward-chaining
• Resolution
20
Unification



We want to find a substitution  such that
x and y match literals
Unify (,) =  if  = 
Some examples
21



Knows(John,x)
Knows(John,
Jane)
{x/Jane}
Knows(John,x)
Knows(y,Michel)
{x/Michel,y/John}
Knows(John,x)
Knows(y,Motherof(y))
{y/John,x/Motherof(John)
Knows(John,x)
Knows(x,Michel)
fail
Standardizing apart eliminates overlap of variables, e.g.,
Knows(z17,Michel)
Unification for example
23
P`1= father-of(Kathy)=Michael
P1= father-of(x)=y
={x/Kathy,y/Michael}
q=ancestor(x,y)
q`=ancestor(Kathy,Michael)
24
25
Example inference using forward
chaining (production systems)
26
Properties of forward-chaining





Sound and complete for first-order definite
clauses
Datalog is first-order definite clauses and no
functions
May not terminate in general if is not entailed
This is unavoidable: entailment with definite
clauses is semi-decidable
Forward chaining is widely used in deductive
databases
27
28
Example inference using backward
chaining
29
Properties of backward-chaining



Depth-first recursive proof search: space is
linear in size of proof
Incomplete due to infinite loops
• Fix by checking current goal against every goal on stack
Inefficient due to repeated subgoals (both
success and failure)
• Fix using cache of previous results (extra space!)

Widely used (without improvements!) for logic
programming (e.g., Prolog)
30
Midterm results

Exams will only be given back to person
the owner of the exam
31