COMP 424 – Artificial Intelligence First Order Logic
Instructors: Jackie CK Cheung and Readings: R&N Ch 8, 9
Propositional logic
Copyright By PowCoder代写 加微信 powcoder
• Propositions are assertions about the state of the world/game/problem. They can be true or false.
• e.g. “Today is Tuesday.”, “Today is Wednesday.”
• Can be combined using logical connectives
• Syntax – specifies the valid sentences in the logic
• Atomic sentences S1, S2, etc. are sentences.
• If S is a sentence, S is a sentence.
• If S1 and S2 are sentences, S1S2 is a sentence.
• If S1 and S2 are sentences, S1S2 is a sentence.
• If S1 and S2 are sentences, S1S2 is a sentence.
• If S1 and S2 are sentences, S1S2 is a sentence.
COMP-424: Artificial intelligence 2
Example: The Wumpus World
• Knowledge from observations: ¬S1,1 ¬S2,1 S1,2
¬B1,1 B2,1 ¬B2,1
• Background knowledge (how the world works):
¬S1,1⇒ ¬W1,1 ∧ ¬W1,2 ∧ ¬W2,1
¬S2,1⇒ ¬W1,1 ∧ ¬W2,1 ∧ ¬W2,2 ∧ ¬W3,1
S1,2⇒ W1,1∨ W1,2∨ W2,2∨ W1,3
We can use inference rules to find out where the Wumpus is!
Describing the world
• Need to describe the world in a more compact and efficient way
• We’d like to be able to describe:
• Objects in the world (e.g., cells, pits, arrows)
• Relationships between objects (cell 1,1 is adjacent to cell 1,2)
• Properties of those objects (cell 2,2 is safe)
• We’d also like to be able to quantify over objects
• e.g., All cells next to a pit are breezy. There is a wumpus
somewhere in the cave.
COMP-424: Artificial intelligence 4
First-order logic (FOL)
• Add a few new elements:
1. Predicates are used to describe objects, properties, relationships.
2. Quantifiers ( = “for all”, = “there exists”) are used for statements that apply to a class of objects.
3. Functions are used to give you an object that is related to another object in a specific way. (e.g., the cell to the RightOf cell 1,1 is cell 2,1)
• These objects (domain elements) are drawn from the domain.
COMP-424: Artificial intelligence 5
Example: FOL sentence
x On(x,Table) → Fruit(x) is a quantifier x is a variable
Table is a constant On is a predicate
Note: Quantifiers allows FOL to handle infinite domains, while propositional local can only handle finite domains.
COMP-424: Artificial intelligence 6
Syntax of FOL: Basic elements
• Connectives , v, ,
• Variables x, y, …
• Ranges over the domain
• Quantifiers ,
• Predicates At(Wumpus,x,y), IsPit(x,y), …
• Map domain element(s) to True/False
• Equality = predicate that checks whether two objects refer to the same domain element
• Functions SonOf(x), PlusOne(x)
• Map domain element(s) to domain element
• Constants map 0 domain elements to a domain element
Wumpus, 2, CS424, …
COMP-424: Artificial intelligence
Types of sentences
Term: constant, variable, function(term1, …, termn)
Atomic sentences predicate(term, term) term1 = term2
e.g. At(Wumpus,2,1) Complex sentences
• Combine atomic sentences using connectives
e.g. At(Wumpus,2,1) → At(Wumpus,1,2)
COMP-424: Artificial intelligence 8
Universal quantification
• Form:
x. Taking(x, AI) → Smart(x)
• This is equivalent to the conjunction of all variable
instantiations
(Taking(Alice, AI) → Smart(Alice)) (Taking(Bob, AI)
→ Smart(Bob)) …
• Typically, → is the main connector with
COMP-424: Artificial intelligence 9
• What does this statement mean? x. Taking(x, AI) Smart(x)
COMP-424: Artificial intelligence 10
• What does this statement mean? x. Taking(x, AI) Smart(x)
Translation is: “Everyone is taking AI and everyone is smart.”
• Common mistake: Using as the main connective with .
COMP-424: Artificial intelligence 11
Existential quantification
• Form:
• This is equivalent to the disjunction of all variable instantiations
(Taking(Alice,AI) Smart(Alice)) (Taking(Bob,AI) Smart(Bob)) …
• Typically, is the main connector with
COMP-424: Artificial intelligence 12
• What does this statement mean? x. Taking(x,AI) → Smart(x)
COMP-424: Artificial intelligence 13
• What does this statement mean? x. Taking(x,AI) → Smart(x)
Problem! This sentence is true if there is anyone who is not taking AI.
Taking(x,AI) → Smart(x) is equivalent to Taking(x,AI)
• Common mistake: Using → as the main connective with . COMP-424: Artificial intelligence 14
Properties of quantifiers
Basic rules:
• x y is the same as y x
• x y is the same as y x
• x y is not the same as y x
COMP-424: Artificial intelligence 15
Properties of quantifiers
Basic rules:
• x y is the same as y x
• x y is the same as y x
• x y is not the same as y x
E.g. x y Loves(x,y) Translate to English? y x Loves(x,y)
COMP-424: Artificial intelligence
Properties of quantifiers
Basic rules:
• x y is the same as y x
• x y is the same as y x
• x y is not the same as y x
E.g. x y Loves(x,y)
“There is a person who loves everyone in the world.”
y x Loves(x,y)
“Everyone in the world is loved by at least one
COMP-424: Artificial intelligence 17
Quantifier duality
• Each quantifier can be expressed by using the other quantifier and negation:
x Loves(x,IceCream) equivalent to x Loves(x,IceCream)
x Loves(x,Broccoli) equivalent to x Loves(x,Broccoli)
COMP-424: Artificial intelligence 18
• Expression term1 = term2 is true under a given interpretation if and only if term1 and term2 refer to the same object in the domain. This is a special predicate!
E.g. x = y 2 = 2
is satisfiable. is valid.
COMP-424: Artificial intelligence
Truth in first-order logic
Sentences are true with respect to a model A model is M = (D, I), where:
• D = Domain of objects
• I = Interpretation:
• Constant symbols → objects
• Predicate symbols → relations over objects
• Basically, definition of the predicates as applied to the domain
• Function symbols → functional relations over objects
• Basically, definition of the functions as applied to the domain
COMP-424: Artificial intelligence 20
Example of truth in FOL
• Suppose we have the sentence: Brother(John, Richard)
• And the model: Domain: D = {R, J}
Interpretation: • Predicates:
Brother: {(J, R), (R, J)} • Functions:
John: J Richard: R
• In this model, Brother(John, Richard) is True.
COMP-424: Artificial intelligence 21
Example of non-truth in FOL
• Suppose we have the sentence: Brother(John, Richard)
• And the model: Domain: D = {R, J}
Interpretation: • Predicates:
Brother: {} • Functions:
John: J Richard: R
• In this model, Brother(John, Richard) is False.
COMP-424: Artificial intelligence 22
Comparison to Propositional Logic
In propositional logic:
• Ontological commitment is to facts
• Specifying whether each proposition symbol is true or false is enough to specify if a sentence is true or false.
• The world is described in terms of objects and relations.
• That’s why we need to specify a model of a world with objects and relations in order to tell if a FOL sentence evaluates to true or false.
COMP-424: Artificial intelligence 23
• Suppose the domain of x and y must be a set of real numbers, and must be the same.
• Suppose > means what you would expect.
• For each of the following sentences, give a domain for which the sentence evaluates to true (if possible), and a domain for which it evaluates to false (if possible)
1. xy x>y 2. xy x>y
COMP-424: Artificial intelligence 24
Inference algorithms for FOL
1. Propositionalize the FOL into propositional logic
• Too expensive for all but the most trivial cases
• See R&N 9.1 for more details
• Forward/backward chaining using generalized modus ponens
3. Resolution
COMP-424: Artificial intelligence 25
Inference in FOL
• Unlike with propositional logic, we have to deal with quantifiers and variables!
• Simple strategy: get rid of the variables and quantifiers to turn it into propositional logic – Propositionalization
• ∀: try for all possible substitutions of the variable e.g., if we know that ∀𝑥. 𝑁𝑖𝑐𝑒(𝑥), replace this with
𝑁𝑖𝑐𝑒Sam,𝑁𝑖𝑐𝑒Aisha,𝑁𝑖𝑐𝑒FatherOfSam …
• ∃: add a new constant symbol (Skolemization)
e.g., if we know that ∃𝑥. 𝑁𝑖𝑐𝑒(𝑥), replace this with 𝑁𝑖𝑐𝑒(SomePerson)
COMP-424: Artificial intelligence 26
Propositionalization – Brief Sketch
Step 1: Get rid of the variables and quantifiers
e.g., Is John evil?
∀𝑥.𝐾𝑖𝑛𝑔 𝑥 ∧𝐺𝑟𝑒𝑒𝑑𝑦 𝑥 →𝐸𝑣𝑖𝑙 𝑥 𝐾𝑖𝑛𝑔 𝐽𝑜h𝑛
𝐺𝑟𝑒𝑒𝑑𝑦 𝐽𝑜h𝑛
𝐵𝑟𝑜𝑡h𝑒𝑟(𝑅𝑖𝑐h𝑎𝑟𝑑, 𝐽𝑜h𝑛)
Get rid of ∀ by applying all possible substitutions of 𝑥:
𝐾𝑖𝑛𝑔 𝐽𝑜h𝑛 ∧ 𝐺𝑟𝑒𝑒𝑑𝑦 𝐽𝑜h𝑛 → 𝐸𝑣𝑖𝑙 𝐽𝑜h𝑛 𝐾𝑖𝑛𝑔 𝑅𝑖𝑐h𝑎𝑟𝑑 ∧ 𝐺𝑟𝑒𝑒𝑑𝑦 𝑅𝑖𝑐h𝑎𝑟𝑑 → 𝐸𝑣𝑖𝑙 𝑅𝑖𝑐h𝑎𝑟𝑑 𝐾𝑖𝑛𝑔 𝐽𝑜h𝑛
𝐺𝑟𝑒𝑒𝑑𝑦 𝐽𝑜h𝑛
𝐵𝑟𝑜𝑡h𝑒𝑟(𝑅𝑖𝑐h𝑎𝑟𝑑, 𝐽𝑜h𝑛)
COMP-424: Artificial intelligence
Propositionalization – Brief Sketch
Step 2: Turn every ground atom into a proposition: 𝐾𝑖𝑛𝑔 𝐽𝑜h𝑛 ∧ 𝐺𝑟𝑒𝑒𝑑𝑦 𝐽𝑜h𝑛 → 𝐸𝑣𝑖𝑙 𝐽𝑜h𝑛
𝐾𝑖𝑛𝑔 𝑅𝑖𝑐h𝑎𝑟𝑑 ∧ 𝐺𝑟𝑒𝑒𝑑𝑦 𝑅𝑖𝑐h𝑎𝑟𝑑 → 𝐸𝑣𝑖𝑙 𝑅𝑖𝑐h𝑎𝑟𝑑 𝐾𝑖𝑛𝑔 𝐽𝑜h𝑛
𝐺𝑟𝑒𝑒𝑑𝑦 𝐽𝑜h𝑛
𝐵𝑟𝑜𝑡h𝑒𝑟(𝑅𝑖𝑐h𝑎𝑟𝑑, 𝐽𝑜h𝑛)
e.g., 𝐾𝑖𝑛𝑔(𝐽𝑜h𝑛) and 𝐺𝑟𝑒𝑒𝑑𝑦(𝐽𝑜h𝑛) are propositions, as are
𝐾𝑖𝑛𝑔(𝑅𝑖𝑐h𝑎𝑟𝑑) and 𝐺𝑟𝑒𝑒𝑑𝑦(𝑅𝑖𝑐h𝑎𝑟𝑑).
Step 3: Run a propositional logic theorem proving algorithm
Complication: if logic has functions, there may be an infinite number of ground atoms in Step 1.
COMP-424: Artificial intelligence 28
Inference algorithms for FOL
1. Propositionalize the FOL into propositional logic
• Too expensive for all but the most trivial cases!
• See R&N 9.1 for more details
• Forward/backward chaining using generalized modus ponens 3. Resolution
COMP-424: Artificial intelligence 29
Proofs in FOL as search
• The proof process can be viewed as a search in which the operators are inference rules:
• And-Introduction (AI)
• Universal Elimination (UE) [aka Universal Instantiation]:
COMP-424: Artificial intelligence 30
Question: Who is faster, Bob or Pat? Proof:
Example Proof
COMP-424: Artificial intelligence 31
Search with Primitive Inference Rules
Operators are inference rules. • MP, IA, UE
States are sets of sentences.
Goal test checks state to see if it contains query sentence.
Solution: Apply standard search techniques!
Problem: Branching factor is huge! Especially for UE.
• Idea: Find a substitution that makes the rule premise
match some known facts
COMP-424: Artificial intelligence 32
Unification
Pattern matching to find promising candidates for UE
We say a substitution unifies atomic sentences p and q if
p = q. e.g.
Assume free variables in table are universally quantified
“If we plug in John for y and Mother(John) for x, the two sides are equal.”
COMP-424: Artificial intelligence
Unification
Idea: Unify complex sentences with known facts to draw conclusions.
e.g., If we know everything in q and also: Knows(John,x) → Likes(John,x)
Then we can conclude:
Likes(John, Jane) Likes(John, Mary) Likes(John, Mother(John))
COMP-424: Artificial intelligence 34
Generalized (GMP)
E.g. p1’ p2’
p1 p2 => q σ
= Faster(Bob,Pat) = Faster(Pat,Steve)
= Faster(x,y) Faster(y,z) => Faster(x,z) = x/Bob, y/Pat, z/Steve
= Faster(Bob,Steve)
COMP-424: Artificial intelligence 35
Generalized (GMP)
E.g. p1’ p2’
p1 p2 => q σ
= Faster(Bob,Pat) = Faster(Pat,Steve)
= Faster(x,y) Faster(y,z) => Faster(x,z) = x/Bob, y/Pat, z/Steve
= Faster(Bob,Steve)
GMP used with KB of Horn clauses (=exactly 1 positive literal):
• a single atomic sentence;
• or a clause of the form: (conjunction of atomic sentences) =>
(atomic sentence).
• All variables assumed to be universally quantified.
COMP-424: Artificial intelligence 36
Completeness in FOL
• Procedure i is complete if and only if:
• GMP is complete for KBs of universally quantified Horn
clauses, but incomplete for general first-order logic.
• Entailment in FOL is only semi-decidable: can find a proof when KB entails α, but not always when KB does not entail α.
• Reduces to Halting Problem: proof may be about to terminate with success or failure, or may go on forever.
COMP-424: Artificial intelligence 37
Inference algorithms for FOL
1. Propositionalize the FOL into propositional logic
• Too expensive for all but the most trivial cases!
• See R&N 9.1 for more details
• Forward/backward chaining using generalized modus ponens
3. Resolution
COMP-424: Artificial intelligence 38
Resolution
Two clauses can be resolved if they contain complementary literals, where one literal unifies with the negation of the other
• Intuition: Like resolution in propositional logic, but taking into account possible unifications
𝐴𝑛𝑖𝑚𝑎𝑙 𝐹 𝑥 ∨𝐿𝑜𝑣𝑒𝑠(𝐺 𝑥 ,𝑥) ¬𝐿𝑜𝑣𝑒𝑠 𝑢,𝑣 ∨¬𝐾𝑖𝑙𝑙𝑠(𝑢,𝑣) resolves to
𝐴𝑛𝑖𝑚𝑎𝑙 𝐹 𝑥 ∨¬𝐾𝑖𝑙𝑙𝑠(𝐺 𝑥 ,𝑥)
𝐿𝑜𝑣𝑒𝑠(𝐺 𝑥 , 𝑥) unifies with ¬𝐿𝑜𝑣𝑒𝑠 𝑢, 𝑣 using substitution 𝜃 =
{𝑢/𝐺 𝑋 , 𝑣/𝑥} COMP-424: Artificial intelligence
Resolution
• Sound and complete inference method for FOL.
• Proof by negation: To prove that KB entails α, instead we
prove that (KB α) is unsatisfiable. • Method:
• The KB and α are expressed in universally quantified, conjunctive normal form.
• Repeat: The resolution inference rule combines two clauses to make a new one.
• Continue until an empty clause is derived (contradiction).
COMP-424: Artificial intelligence 40
Conjunctive Normal Form in FOL
• Literal = (possibly negated) atomic sentence, e.g., Rich(Me)
• Clause = disjunction of literals, e.g. Rich(Me) v Unhappy(Me)
• The KB is a big conjunction of clauses.
E.g. Rich(x) v Unhappy(x) Rich(Me)
Unhappy(Me) with σ={x / Me}
COMP-424: Artificial intelligence 41
Converting a KB to CNF
1. Replace PQ by P v Q
2. Move inwards, e.g. x P becomes x P
3. Standardize variables apart, e.g. x P v x Q becomes x P v y Q
4. Move quantifiers left in order, e.g. x P v y Q becomes xy Pv Q
5. Eliminate existential quantifiers by Skolemization
COMP-424: Artificial intelligence 42
Skolemization
• We want to get ride of existentially quantified variables: x Rich(x) becomes Rich(G1)
where G1 is a new Skolem constant.
• It gets more tricky when is inside e.g. “Everyone has a heart”
x Person(x) y Heart(y) Has(x,y)
How should we replace y here?
• Incorrect: x Person(x) Heart(H1) Has(x,H1)
• Correct: x Person(x) Heart(H(x)) Has(x,H(x))
where H is a new symbol called a Skolem function.
COMP-424: Artificial intelligence 43
Converting a KB to CNF
1. Replace PQ by P v Q
2. Move inwards, e.g. x P becomes x P
3. Standardize variables apart, e.g. x P v x Q becomes x P v y Q
4. Move quantifiers left in order, e.g. x P v x Q becomes xy Pv Q
5. Eliminate existential quantifiers by Skolemization
6. Drop universal quantifiers
7. Distribute over v, e.g. (P Q) v R becomes (P v R) (Q v R)
COMP-424: Artificial intelligence
Jack owns a dog.
Every dog owner is an animal lover.
No animal lover kills an animal.
Either Jack or Curiosity killed the cat, who is named Tuna.
Did Curiosity kill the cat?
COMP-424: Artificial intelligence
Sentences + background knowledge
Original Sentences (Plus Background Knowledge)
COMP-424: Artificial intelligence 46
Example: Conjunctive Normal Form
Conjunctive Normal Form
(D is a placeholder for the dogs unknown name (i.e. Skolem symbol/function). Think of D like “JohnDoe”)
COMP-424: Artificial intelligence 47
Example: Proof
COMP-424: Artificial intelligence 48
Resolution Strategies
Heuristics that impose a sensible order on the resolutions we attempt
• Unit resolution: prefer to perform resolution if one clause is just a literal – yields shorter sentences.
• Set of support: identify a subset of the KB (hopefully small); every resolution will take a clause from the set and resolve it with another sentence, then add the result to the set of support.
• Can make inference incomplete!
• Input resolution: always combine a sentence from the query
or KB with another sentences. Not complete in general.
COMP-424: Artificial intelligence 49
Proofs can be lengthy!
Simple problem
COMP-424: Artificial intelligence 50
Applications of FOL
• Expert systems
• Prolog: a logic programming language
• Production systems
• Semantic nets
• Automated theory proving
• Planning
COMP-424: Artificial intelligence 51
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com